[new release] hol2dk (2.1.0) #28937
Merged
[new release] hol2dk (2.1.0) #28937
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
CHANGES: ### Added - command nbp to print the number of (useful) proofs - command files to print theorem statements following the file structuration in HOL-Light - command thms to print theorems (named or not) proved in a file - command unsplit to put the proofs of all the theorems proved in a HOL-Light file in the same Lambdapi file - command concl to print the statements of theorems between two indexes - option --max-dup $k to share the proof of a theorem if it is duplicated more than $k times - renamings to handle the Multivariate library - test/Sig_mappings_N.v and test/Sig_With_N.v: axiomatizations of mappings_N.v and With_N.v respectively - test/Makefile: generates Spec_mappings_N.v and Spec_With_N.v, standalone versions of Sig_mappings_N.v and Sig_With_N.v, and checks the correctness of mappings_N.v and With_N.v wrt to those specification files the use of Spec_With_N.v instead of With_N.v allows to reduce the Coq checking time of Multivariate/make_complex.ml by 40% (21 hours instead of 35 hours) ### Changed - command link renamed into config and improved - update to work with HOL-Light 3.1 and Rocq 9.0 - minimize dependencies in spec files - theory_hol.lp: rename T into ⊤ and F into ⊥ ### Fixed - handling of type variables occurring in a proof but not in a statement
jmid
approved these changes
Nov 21, 2025
Member
jmid
left a comment
jmid
left a comment
There was a problem hiding this comment.
All green (modulo what appears to be a network issue triggering on MSys2), thanks!
Would you consider adding an x-maintenance-intent entry?
https://github.com/ocaml/opam-repository/blob/master/governance/policies/archiving.md
Contributor
Author
|
Yes. Should we write something like the following? |
Member
|
Yes, that would be perfect! 👍 |
Contributor
Author
|
Note that the emacs mode for opam does not color this field. |
Member
|
Thanks |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
HOL-Light to Dedukti/Lambdapi and Rocq translator
CHANGES:
Added
command nbp to print the number of (useful) proofs
command files to print theorem statements following the file structuration in HOL-Light
command thms to print theorems (named or not) proved in a file
command unsplit to put the proofs of all the theorems proved in a HOL-Light file in the same Lambdapi file
command concl to print the statements of theorems between two indexes
option --max-dup $k to share the proof of a theorem if it is duplicated more than $k times
renamings to handle the Multivariate library
test/Sig_mappings_N.v and test/Sig_With_N.v: axiomatizations of mappings_N.v and With_N.v respectively
test/Makefile: generates Spec_mappings_N.v and Spec_With_N.v, standalone versions of Sig_mappings_N.v and Sig_With_N.v, and checks the correctness of mappings_N.v and With_N.v wrt to those specification files
the use of Spec_With_N.v instead of With_N.v allows to reduce the Coq checking time of Multivariate/make_complex.ml by 40% (21 hours instead of 35 hours)
Changed
Fixed