Skip to content

1.0.0
Compare
Choose a tag to compare
@fblanqui fblanqui released this 25 Feb 08:59
· 59 commits to main since this release
1.0.0
3330bf7
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.

CHANGES:

Added

  • 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

Modified

  • identifier renamings
  • merged the command dg in the command mk
  • fusion.ml: do not generate new theorems for empty instantiations

Fixed

  • valid dedukti and lambdapi identifiers
Assets 3
Loading