All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
Big improvements in Lambdapi and Coq file generation time, and Coq checking time.
- hol2dk can now generate term abbreviations and proofs in several files
in parallel:
- The option --max-size-abbrev allows to fix the maximum size for term abbreviations files.
- The option --max-size-proof allows to fix the maximum size for proof files.
- optimization of lp file dependencies in generated lp files.
- generation of Makefile lpo dependencies at the same time as lp files.
- Makefile: lpo and vo dependencies are recomputed automatically.
- FILES_WITH_SHARING renamed into BIG_FILES and not added by add-links anymore
- command dump[-simp]-use renamed into dump[-simp]-before-hol
- for each theorem, two files are generated: one with the proof, and one declaring the theorem as an axiom
- add-links script
- command rewrite to simplify prf files
- command purge to compute useless theorems these two commands greatly reduce the size of generated proofs
- command simp is equivalent to rewrite and purge
- command dump-simp is equivalent to dump, pos, use and simp
- allow simultaneous dumping
- alignments of the types option, Sum, list, char, nadd
- command split to generate a pos/use/sti/nbp file for each named theorem (an sti file contains the starting index of the corresponding proof)
- command theorem to generate the lp files corresponding to a named theorem
- Makefile to generate and check lp and coq files generated with split
- command size to get statistics on the size of terms
- option --print-stats to print statistics on hash tables at exit
- use hash tables instead of maps to build abbreviations maps
- use sharing when building canonical types and terms
- add option --use-sharing for using sharing in lp output when defining term abbreviations
- command nbp to get the number of proof steps
- commands patch, unpatch and link to call the corresponding scripts
- command env to print $HOL2DK_DIR and $HOLLIGHT_DIR
- identifier renamings
- merged the command dg in the command mk
- fusion.ml: do not generate new theorems for empty instantiations
- valid dedukti and lambdapi identifiers
- add command dump-use for dumping a file without including "hol.ml"
- rename mk-part command into mk
- the dump command now includes "hol.ml"
- do not print ocaml warnings while dumping proofs
- do not export unused proofs (about 7%)
- make hol2dk stat give the number of unused proofs
- README.md
- output of hol2dk axm
- output of hol2dk mk
First release.