Port coq-plugin-lib to Coq 8.11 #42
Conversation
Note: this introduces a breaking change with the type signatures of one of the helper functions . . .
Makefile.local
Outdated
| @@ -0,0 +1 @@ | |||
| OCAMLWARN=-warn-error +a-3-8-40-32-28 | |||
There was a problem hiding this comment.
Coq 8.11 now turns all warnings into errors. This line is necessary to turn the errors (which were formerly warnings) back to warnings. I took a whitelist approach just to be safe, so only the following warnings: 3, 8, 40, 32, and 28 are kept as warnings.
| @@ -140,6 +140,9 @@ let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list = | |||
| match (l1, l2, l3) with | |||
| | ([], [], []) -> | |||
| [] | |||
| | ([], _, _) -> failwith "Mismatched sized lists passed to map3" | |||
There was a problem hiding this comment.
These lines were initially defined to address the warning that the pattern matching is not exhaustive. Since I've manually marked this category of warnings to be kept as warnings, this is a bit redundant. I've left this here to give more useful error messages at runtime. Let me know if I should remove them.
| @@ -23,3 +23,4 @@ plugin/Makefile | |||
| plugin/.merlin | |||
| *.out | |||
| _opam | |||
| src/plibrary.ml | |||
There was a problem hiding this comment.
I excluded this from git because it appears to be a build artifact that gets generated whenever build.sh is run.
src/coq/decompiler/decompiler.ml
Outdated
|
|
||
| let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in | ||
| let (p', _, _) = Proof.run_tactic env tac p in | ||
| let compact_p = Proof.data (Proof.compact p') in |
There was a problem hiding this comment.
Perhaps Proof.compact is unnecessary? Idk if this is actually needed.
| @@ -117,7 +112,7 @@ let try_register_record mod_path (ind, ind') = | |||
| * | |||
| * TODO sigma handling, not sure how to do it here/if we need it | |||
| *) | |||
| let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Globnames.Refset.empty) ident tr_constr mod_body = | |||
| let transform_module_structure env ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body = | |||
There was a problem hiding this comment.
I added env as an arg to this func, not sure if this is necessary. TODO: consider removing it.
| let sigma = Evd.restrict_universe_context sigma uvars in | ||
| let univs = Evd.check_univ_decl ~poly sigma udecl in | ||
| let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) | ||
| let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in |
There was a problem hiding this comment.
Should use ~allow_evars:true
There was a problem hiding this comment.
Ok just pushed the fix -- it seems to work!
This PR ports coq-plugin-lib to Coq 8.11. It is a work in progress (documentation was a bit sparse so I had to guess in a few places by looking at the types). I've marked this as a draft PR, but it's ready for critique and feedback. Hopefully it works!
Some other notes: Coq 8.11 (released January 2020) is the earliest version of Coq that my ARM mac supports. This PR will enable folks with M1/M2 macs to use this lib.