anil.recoil.org / opam-repository
this repo has no description
0
fork

Configure Feed

Select the types of activity you want to include in your feed.

[new release] hol2dk (2.0.0)

CHANGES:

Big improvements in Lambdapi and Coq file generation time, and Coq checking time.

### Added

- 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.

### Changed

- 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

Frédéric Blanqui 2cf93e05 f2df0b10

+38
+38
packages/hol2dk/hol2dk.2.0.0/opam
··· 1 + opam-version: "2.0" 2 + synopsis: "HOL-Light to Dedukti/Lambdapi and Coq translator" 3 + description: "HOL-Light to Dedukti/Lambdapi and Coq translator" 4 + maintainer: ["Frédéric Blanqui"] 5 + authors: ["Frédéric Blanqui" "Anthony Bordg"] 6 + license: "CeCILL-2.1" 7 + homepage: "https://github.com/Deducteam/hol2dk" 8 + doc: "https://github.com/Deducteam/hol2dk/blob/master/README.md" 9 + bug-reports: "https://github.com/Deducteam/hol2dk/issues" 10 + depends: [ 11 + "ocaml" {>= "4.13"} 12 + "dune" {>= "3.7"} 13 + "odoc" {with-doc} 14 + ] 15 + build: [ 16 + ["dune" "subst"] {dev} 17 + [ 18 + "dune" 19 + "build" 20 + "-p" 21 + name 22 + "-j" 23 + jobs 24 + "@install" 25 + "@runtest" {with-test} 26 + "@doc" {with-doc} 27 + ] 28 + ] 29 + dev-repo: "git+https://github.com/Deducteam/hol2dk.git" 30 + url { 31 + src: 32 + "https://github.com/Deducteam/hol2dk/releases/download/2.0.0/hol2dk-2.0.0.tbz" 33 + checksum: [ 34 + "sha256=1a91f3c3743575506c7e727a8615586182d7a7a40e756da2908890b5e4310fb2" 35 + "sha512=14d15456d36a399c8842581bf111575a16c5d64c162b31e9b0f5b57a0ce35ae9cd560ff5164997525f5737bd66a117c1977a6d07302c318c46c6b65be2629e3b" 36 + ] 37 + } 38 + x-commit-hash: "0059a181e647ba00b2aa8806966fa3b61724ae1b"