Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Primitive flags #1032

Closed
wants to merge 139 commits into from
Closed

Primitive flags #1032

wants to merge 139 commits into from

Conversation

mattam82
Copy link
Member

Add a way to control the presence of primitive ints/floats or arrays in terms (useful for correctness statements about translations which do not yet support arrays, or any primitive types).

mrhaandi and others added 30 commits April 4, 2023 05:41
@mrhaandi @mattam82
improved auto goal selection (#737)
1a7d230
@mrhaandi @mattam82
prepare for coq/coq#16289 (#734)
7d1b643
@ppedrot @mattam82
Adapt w.r.t. coq/coq#16442.
2e1085a
@mattam82
ML fixes
6219522
@mattam82
Adapt to Coq 8.17
7399921
@mattam82
Update opam packages
0d08380
@mattam82
Update github action coq version
6f72fe9
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
83cea47
@mattam82
Usage for make-opam-files
66e7d31
@mattam82
Fix dep in opam file
76e8e48
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
ea7b244
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
4b975ae
@mattam82
Fix due to high priority existT hint in core
66f6857
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
f867f01
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
e61cd19
@mattam82
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
736ac17
@mattam82
Update install instructions for Coq 8.17
1f9ed65
@mattam82
Merge branch 'coq-8.16' into coq-8.17
c27c302
@mattam82
Fix sprop_level/prop_level requring lazy evaluation
198e202
@yforster
close some computational obligations with defined in erase_global_decls
f91a1e7
@mattam82
Move nix actions away
e578a02
@mattam82
Merge pull request #961 from yforster/fix-qed-problem
bb34a12 
Close computational obligations with defined in erase_global_decls
@yforster
Invariants in named recursion rule (#967)
14ad024
@mattam82
Update Makefile to install erasure plugin
c065ed6
@mattam82
Fix sneaky, useless Prop <= Type use that was breaking certified erasure
e0794e3
@dependabot
Bump actions/checkout from 3 to 4 (#978)
3e0f857
@tabareau
improve stengthening to get cumul info on type
adba794
@tabareau
more general strengthening
9fd6f61
@tabareau
Merge pull request #985 from MetaCoq/improve-strengthening
46be926 
improve strengthening to get cumul info on type
@tabareau
remove parameters in firstorder inductive types
be44477
JasonGross and others added 29 commits December 3, 2023 09:51
@JasonGross
Fix quotation after primitive array support
dd498ea
@JasonGross
Revert "Disable the opam quotation package for now"
ffc04ea 
This reverts commit 7dd6de8.
@JasonGross
Revert "Disable quotation opam module dependency"
3f0d369 
This reverts commit 1dd8994.
@JasonGross
Revert "Disable quotation module build"
3a51898 
This reverts commit 8b4d7a9.
@JasonGross
Merge pull request #1024 from JasonGross/coq-8.17+restore-quotation
d6acef9 
Fix quotation after primitive array support
@mattam82
Merge branch 'coq-8.17' into LSP-support
ecf08b7
@mattam82
Merge pull request #1006 from yannl35133/LSP-support
aec0e80 
LSP Support
@mattam82
Evaluation for arrays
022608f
@mattam82
Adapt evaluation to primitive arrays (including PCUIC)
822cb61
@mattam82
Adapted erasure to new array evaluation rules, except named wcbveval …
69a80fc 
…relation
@mattam82
Adapt WcbvEvalNamed to primitives (new values)
4d6d014
@mattam82
Merge pull request #1027 from MetaCoq/primitive-arrays-eval
943772d 
Primitive evaluation
@mattam82
Adapted extraction correctness, only remaining wf_glob proofs
5e9ae4f
@mattam82
WIP on wellformedness proof
e60bf4d
@mattam82
Finished proof of correctness for typed erasure
40d2284
@mattam82
Generalized theorems for typed optimization
f7918c3
@mattam82
Typed erasure variant
c2620bb
@mattam82
Prove that dearging preserves eta-expanded constructors and fixpoints…
ea4ab2d 
… (tricky!)
@mattam82
Finish the proof of preservation of eta-expansion by dearging
f1a445b
@mattam82
Merge pull request #1030 from MetaCoq/typed-extraction-integration
b646cd3 
Typed extraction integration
@yannl35133
More unified "judgment" type
8a07c40
@yannl35133
More unified All_local_env, cleaned up {PCUIC,}Typing
c9f169b
@yannl35133
Shared app_context, integrated Σ in ctx_inst
9b74e81
@yannl35133
Change typing rules for lambda prod and letin
e4a179c
@yannl35133
Rename LevelAlg -> Universe.t -> Sort.t, equality takes conv_pb
3a488f5
@yannl35133
Fix translations
078344e
@mattam82
Merge pull request #1007 from yannl35133/rejudgment
e9b17dc 
More unified judgment type and All_local_env
@mattam82
Make EPrimitive universe polymorphic so it can apply to term types in…
c1414bf 
… Set or Type
@mattam82
Add an EPrimitiveFlags to control the presence of ints/floats/arrays
f526608
@mattam82 mattam82 closed this Jan 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@mattam82 @mrhaandi @ppedrot @yforster @tabareau @yannl35133 @JasonGross