Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
32a0b4e
Ported deftorel pass
DCupello1 Nov 4, 2025
d28d305
Added fallthrough semantics to converted defs, which conveniently han…
DCupello1 Nov 18, 2025
7df8c60
Merge branch 'improve-ids-pass' into deftorel-pass
DCupello1 Nov 19, 2025
c3d6045
Merge branch 'improve-ids-pass' into deftorel-pass
DCupello1 Dec 8, 2025
2be03e5
Remove created relations out of recursive groups if they don't call t…
DCupello1 Dec 8, 2025
9d24f4e
Added a filter to the prems from the generated fallthrough relations …
DCupello1 Dec 8, 2025
589bccc
Let introduction pass
DCupello1 Jan 13, 2026
6bd6632
Fix on improve ids related to let premise
DCupello1 Jan 13, 2026
5a6957b
Fix tests
DCupello1 Jan 13, 2026
2ef2c5e
Else simplification pass in progress
DCupello1 Jan 14, 2026
0d763f8
exposing hints from else and wf relations
DCupello1 Jan 14, 2026
c3f581a
Modification to else relation removal, only removes if there are no u…
DCupello1 Jan 15, 2026
3a2454e
Merge branch 'letintro-pass' into else-simp-pass
DCupello1 Jan 15, 2026
fe65f4f
fix tests
DCupello1 Jan 15, 2026
066a296
fix tests, adding wf relations again (removed by accident)
DCupello1 Jan 19, 2026
6e28e18
Changed generated otherwise to be conjunction instead of disjunction.
DCupello1 Jan 20, 2026
67c5e56
fix tests
DCupello1 Jan 20, 2026
beac0dc
Merge branch 'main' into deftorel-pass
DCupello1 Jan 20, 2026
122dc2d
Made fallthrough only when otherwise is present. Refactored a bit usi…
DCupello1 Jan 20, 2026
3d64cfb
Removed subtyping matching check
DCupello1 Jan 20, 2026
f4f1fc8
reordering so generated deftorel relations get implicit sidecondition…
DCupello1 Jan 20, 2026
9c4be10
Merge branch 'main' into deftorel-pass
DCupello1 Jan 21, 2026
f21f9b7
move rocq translation to single branch
DCupello1 Nov 19, 2025
4a8cfb8
Ensures that ids do not clash with reserved ids. Mixops also cannot b…
DCupello1 Nov 19, 2025
41bc410
Remove aliasing in mut checks since done in alias-mut pass now
DCupello1 Nov 19, 2025
af7bc34
Made naive name resolving for now to make rocq compile.
DCupello1 Nov 20, 2025
3c0dd9a
Added removal overlapping check only for rocq for now.
DCupello1 Nov 20, 2025
0fc4513
enable ITE introduction pass and added specific rendering to rocq
DCupello1 Dec 8, 2025
5fc2688
Added extra clause to functions with type families.
DCupello1 Jan 22, 2026
8efa035
Added inhabited check for type variables in function definitions.
DCupello1 Jan 22, 2026
5cbf224
Made recursive functions into relations due to not having immediate c…
DCupello1 Jan 22, 2026
ef63432
small fix on sub to allow for nested sub transformation.
DCupello1 Jan 26, 2026
9c182a9
Once again, turning premises of an else relation into disjunction, an…
DCupello1 Jan 26, 2026
5fb9006
Merge branch 'else-simp-pass' into rocq-backend
DCupello1 Jan 26, 2026
c942181
Fix recursive functions with hints being filtered out.
DCupello1 Jan 26, 2026
3ab9cc5
Enabled else simplification and improve notation for list access, lis…
DCupello1 Jan 26, 2026
0f4d886
Made uncase projection functions into coercions for nicer output.
DCupello1 Jan 27, 2026
98e29a2
Made disambiguation pass (which has name mangling as a fallback solut…
DCupello1 Jan 27, 2026
cf642f4
Moved overlapping clauses removal to disambiguation pass, and made un…
DCupello1 Jan 27, 2026
e680422
Improve ids change: Now ensures variables don't have same name as con…
DCupello1 Jan 27, 2026
8cd4fe4
Removed disambiguation for mixops of more than 1 atom, since its name…
DCupello1 Jan 27, 2026
c0fb9f0
Disambiguation for mixop is now supported: it is turned into a simple…
DCupello1 Jan 27, 2026
fc78173
Made most list operations into seq from ssreflect
DCupello1 Feb 11, 2026
ad9484b
Undep: made type family wf relations necessary
DCupello1 Feb 11, 2026
e688543
Modified some seq functions from imported code
DCupello1 Feb 17, 2026
16b70bd
Rebase the lean4 wip code onto rocq-backend
nomeata Feb 19, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions .github/workflows/ci-lean.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
name: CI Lean4


on:
push:
branches: [ main ]
paths: [ spectec/**, document/** ]

pull_request:
branches: [ main ]
paths: [ spectec/**, document/** ]

jobs:
test-lean:
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v4
- name: Install Elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Run Lean.wasm
working-directory: spectec/test-lean4
run: |
lean Wasm.lean
5 changes: 5 additions & 0 deletions spectec/backend-lean4/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
(library
(name backend_lean4)
(libraries il)
(modules print)
)
Loading