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

[new release] hol2dk (1.0.0)

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

Frédéric Blanqui 0758a2c8 90d8c520

options
unified split
Changed files
+37
packages
hol2dk
hol2dk.1.0.0
opam
+37
packages/hol2dk/hol2dk.1.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

       
+

       
bug-reports: "https://github.com/Deducteam/hol2dk/issues"


     

       

       
9

       
+

       
depends: [


     

       

       
10

       
+

       
  "ocaml" {>= "4.13"}


     

       

       
11

       
+

       
  "dune" {>= "3.7"}


     

       

       
12

       
+

       
  "odoc" {with-doc}


     

       

       
13

       
+

       
]


     

       

       
14

       
+

       
build: [


     

       

       
15

       
+

       
  ["dune" "subst"] {dev}


     

       

       
16

       
+

       
  [


     

       

       
17

       
+

       
    "dune"


     

       

       
18

       
+

       
    "build"


     

       

       
19

       
+

       
    "-p"


     

       

       
20

       
+

       
    name


     

       

       
21

       
+

       
    "-j"


     

       

       
22

       
+

       
    jobs


     

       

       
23

       
+

       
    "@install"


     

       

       
24

       
+

       
    "@runtest" {with-test}


     

       

       
25

       
+

       
    "@doc" {with-doc}


     

       

       
26

       
+

       
  ]


     

       

       
27

       
+

       
]


     

       

       
28

       
+

       
dev-repo: "git+https://github.com/Deducteam/hol2dk.git"


     

       

       
29

       
+

       
url {


     

       

       
30

       
+

       
  src:


     

       

       
31

       
+

       
    "https://github.com/Deducteam/hol2dk/releases/download/1.0.0/hol2dk-1.0.0.tbz"


     

       

       
32

       
+

       
  checksum: [


     

       

       
33

       
+

       
    "sha256=b9a304e56acda8367944c8590497ede7a386850b423432186309f36cc3aaed98"


     

       

       
34

       
+

       
    "sha512=80027e2966d0b4192b5c297b6932ce10d7f20890be93e3f20570afb0ecd3b0b8f0ae84438a1f1aca5e8839e157240de8aedc772b3087c79b5c9ff2dca7792e7c"


     

       

       
35

       
+

       
  ]


     

       

       
36

       
+

       
}


     

       

       
37

       
+

       
x-commit-hash: "3330bf799499a8e452fdb5e578f4936ee7c18a25"