]> matita.cs.unibo.it Git - helm.git/commitdiff
Enable "dune build -p matita" + version bumped to 0.99.5
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 2 Jan 2023 21:29:33 +0000 (22:29 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Feb 2023 14:23:41 +0000 (15:23 +0100)
25 files changed:
matita/components/content/dune
matita/components/content_pres/dune
matita/components/disambiguation/dune
matita/components/extlib/dune
matita/components/getter/dune
matita/components/grafite/dune
matita/components/grafite_engine/dune
matita/components/grafite_parser/dune
matita/components/library/dune
matita/components/logger/dune
matita/components/ng_cic_content/dune
matita/components/ng_disambiguation/dune
matita/components/ng_extraction/dune
matita/components/ng_kernel/dune
matita/components/ng_library/dune
matita/components/ng_paramodulation/dune
matita/components/ng_refiner/dune
matita/components/ng_tactics/dune
matita/components/registry/dune
matita/components/syntax_extensions/dune
matita/components/xml/dune
matita/configure.ac
matita/dune-project
matita/matita.opam
matita/matita/dune

index df473bb5b001bdfc805b41889af757113ef5d558..bcaa095529d4a570821ac4a042301f0d8acced0b 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_library helm_ng_kernel)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index bb909617671eb2f0afb66496e52b60163e712754..c5f2c3923b17c34000ef6ca661b259ddea09b9d5 100644 (file)
@@ -5,5 +5,5 @@
  (preprocessor_deps ../syntax_extensions/pa_unicode_macro.cma ../syntax_extensions/helm_syntax_extensions.cma)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-27)))) ; -27 is for generated files :-(
index 0b89f82dc6a7a0e9b6c5670648de7ee302ab3980..5f22ba2f2ad4635556e7ae08f98ea20d9d55a372 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_content)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index a81b6d6465025f441a89e6ab57441c2b265b10d1..83a3784e1f9e572f771658cf69ba53001dc847f6 100644 (file)
@@ -3,5 +3,5 @@
  (libraries str unix camlp5.gramlib)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 4356f0fe6b231eb3e5628d9809233516b18b53a4..102e262efc505ace84a4fad88b624bcc9976f97b 100644 (file)
@@ -5,5 +5,5 @@
  (wrapped false)
  (modules (:standard \ test)))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 7deeb70bec8120999bbc846f13196fff312d3abe..41550f1889fa0906eb0df950656a3c661331a367 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_content helm_ng_kernel)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index a40b337949f0036dce697cbaf8f1298895b56bd8..5370981e9a7478a9503f343025516de7a0eb9af5 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_grafite_parser helm_ng_tactics helm_ng_extraction)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 329efec92544ad31e792a5dfe6cf0d1806b3708a..22aa2475b0ad4561366c68cda780e1c44b5a98e5 100644 (file)
@@ -5,5 +5,5 @@
  (preprocessor_deps ../syntax_extensions/pa_unicode_macro.cma ../syntax_extensions/helm_syntax_extensions.cma)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-27)))) ; -27 is for generated files :-(
index cf880522f38cbfcf55fcff5bccb6b8ae42464626..47c9d307186f8941ca6f2e39a4e0625a972573b4 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_getter)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 4313f42a430c38cc5dc6d0a52cb5748ef68dc089..029fb06bd88f5dec4ca668d653dde4125aacf44e 100644 (file)
@@ -2,5 +2,5 @@
  (name helm_logger)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 66853b1e1de9432b5e5ac4efff2096725d245500..ed7eb41a7ffd075e25d341b3ac15bbe5e1024711 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_library helm_ng_library helm_grafite helm_content helm_ng_refiner)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index dd7b556ce056f0374e8346326ce93f1097154146..2ff739a9c5196ee45a97e5ba3ea77d583bb324f6 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_ng_cic_content helm_ng_refiner helm_disambiguation)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 92f7d14f254fe50f31092097ec050aad9db688fe..af72467698b0ab699f7900648cc00a6f15b8ed6d 100644 (file)
@@ -4,5 +4,5 @@
  (preprocess (action (system "camlp5o %{input-file}")))
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 4bd483ca890009a91e2bbaae3eccb5395904a0dd..c0564318e2ea0ab5c885f75a2a13e57b63eb7856 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_extlib)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index efb88ef688344267aedd1a05717216c43650fd5c..bc4fe3bcedb27660314555d248fb5a566a0a00a3 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_ng_refiner helm_registry helm_library)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index be0a28530a685e6a90a3f759ffa341f2d5d0f446..cf0544396ef756b5c99a84b7cefbec17a499ab60 100644 (file)
@@ -5,5 +5,5 @@
  (foreign_stubs (language c) (names hash)
    (include_dirs %{ocaml_where}/caml)))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 72b3f7b4a0998b617034d1782c6f704964b2e896..cb6b5688a9190222feb0abfffdc498d2d84c9f01 100644 (file)
@@ -4,5 +4,5 @@
  (wrapped false)
  (modules (:standard \ oMeta2nMeta)))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 473674ab2a22255cf0d5312e8cd45fe2861005be..b2d38160f5e4ef420df2e290774f6a6649334bd7 100644 (file)
@@ -3,5 +3,5 @@
  (libraries helm_ng_disambiguation helm_ng_paramodulation)
  (wrapped false))
 (env
-  (dev
+  (_
     (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index 15b3173b72f5bebb75c9ffdb2869c962094a4429..10dcf81883e7c7dfcd1104d8e231264fa92944c9 100644 (file)
@@ -5,5 +5,5 @@
  (wrapped false)
  (modules (:standard \ test)))
 (env
-  (dev
+  (_
     (flags (:standard -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index c780ece7f51746f55535451cd7870973521717b5..e7d02a81c0146b543d114f9a4505b8ce828616c8 100644 (file)
@@ -32,5 +32,5 @@
  (action (run ./make_table.exe utf8MacroTable.ml utf8MacroTable.ml.txt)))
 
 (env
-  (dev
+  (_
     (flags (:standard -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index fb60d63c67427df1a3a6c4bb9346f3bd59c367b0..ba113bd7074e7952f679a30d34a27488acc7f415 100644 (file)
@@ -5,5 +5,5 @@
  (wrapped false)
  (modules (:standard \ test)))
 (env
-  (dev
+  (_
     (flags (:standard -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50))))
index ba25fab4df555843fd60d3b4cb820bded94c27d6..cf8a8e4ee8985c816c78f13b5e55b39fc432a2c1 100644 (file)
@@ -6,7 +6,7 @@ AC_CONFIG_SRCDIR([matita/matitaTypes.ml])
 DEBUG_DEFAULT="true"
 DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
 RT_BASE_DIR_DEFAULT="`pwd`/matita"
-MATITA_VERSION="0.99.4"
+MATITA_VERSION="0.99.5"
 DISTRIBUTED="yes"  # "yes" for distributed tarballs
 # End of distribution settings
 
index 99912ea13758d64c57cf83a62063047435703826..4dbce59a9abec53492ea1c74cd51e618152184e0 100644 (file)
@@ -2,25 +2,34 @@
 
 (name matita)
 
+(version 0.99.5)
+
 (generate_opam_files true)
 
 (source
- (github username/reponame))
+ (uri http://matita.cs.unibo.it/download.shtml))
+
+(authors "HELM Team (Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli et alt.)")
 
-(authors "Author Name")
+(maintainers "Claudio Sacerdoti Coen")
 
-(maintainers "Maintainer Name")
+(license GPL)
 
-(license LICENSE)
+(homepage http://matita.cs.unibo.it)
 
-(documentation https://url/to/documentation)
+(documentation http://matita.cs.unibo.it)
 
 (package
  (name matita)
- (synopsis "A short synopsis")
- (description "A longer description")
- (depends ocaml dune)
+ (synopsis "An experimental, interactive theorem prover")
+ (description "Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna.")
+ (depends
+   (ocamlnet (= 4.1.9.git))
+   (ulex-camlp5 (= 1.3))
+   (ocaml-expat (= 1.1.0))
+   (lablgtk3-sourceview3 (= 3.1.3))
+   (camlp5 (= 8.00.04)))
  (tags
-  (topics "to describe" your project)))
+  ("interactive theorem proving" "calculus of constructions")))
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
index 5e02c0e593d4c343c4f574bc91b9b6432b2dcb28..bba4c6547fd93a5dd118551c9cf475fec2d4a6f7 100644 (file)
@@ -1,17 +1,24 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "A short synopsis"
-description: "A longer description"
-maintainer: ["Maintainer Name"]
-authors: ["Author Name"]
-license: "LICENSE"
-tags: ["topics" "to describe" "your" "project"]
-homepage: "https://github.com/username/reponame"
-doc: "https://url/to/documentation"
-bug-reports: "https://github.com/username/reponame/issues"
+version: "0.99.5"
+synopsis: "An experimental, interactive theorem prover"
+description:
+  "Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna."
+maintainer: ["Claudio Sacerdoti Coen"]
+authors: [
+  "HELM Team (Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli et alt.)"
+]
+license: "GPL"
+tags: ["interactive theorem proving" "calculus of constructions"]
+homepage: "http://matita.cs.unibo.it"
+doc: "http://matita.cs.unibo.it"
 depends: [
-  "ocaml"
   "dune" {>= "3.6"}
+  "ocamlnet" {= "4.1.9.git"}
+  "ulex-camlp5" {= "1.3"}
+  "ocaml-expat" {= "1.1.0"}
+  "lablgtk3-sourceview3" {= "3.1.3"}
+  "camlp5" {= "8.00.04"}
   "odoc" {with-doc}
 ]
 build: [
@@ -28,4 +35,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/username/reponame.git"
+dev-repo: "http://matita.cs.unibo.it/download.shtml"
index 3a59004f73eadd92eca51bb893089b35d74ad26b..1c87a72695fdb569c0728ab4c3b8df9a26c5ea42 100644 (file)
@@ -22,5 +22,5 @@
  (modules matitac matitaclean))
 
 (env
-  (dev
+  (_
     (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings