From 516c0e7f030a485b3a1d91fdc1c536d2b4270997 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Jan 2023 22:29:33 +0100 Subject: [PATCH] Enable "dune build -p matita" + version bumped to 0.99.5 --- matita/components/content/dune | 2 +- matita/components/content_pres/dune | 2 +- matita/components/disambiguation/dune | 2 +- matita/components/extlib/dune | 2 +- matita/components/getter/dune | 2 +- matita/components/grafite/dune | 2 +- matita/components/grafite_engine/dune | 2 +- matita/components/grafite_parser/dune | 2 +- matita/components/library/dune | 2 +- matita/components/logger/dune | 2 +- matita/components/ng_cic_content/dune | 2 +- matita/components/ng_disambiguation/dune | 2 +- matita/components/ng_extraction/dune | 2 +- matita/components/ng_kernel/dune | 2 +- matita/components/ng_library/dune | 2 +- matita/components/ng_paramodulation/dune | 2 +- matita/components/ng_refiner/dune | 2 +- matita/components/ng_tactics/dune | 2 +- matita/components/registry/dune | 2 +- matita/components/syntax_extensions/dune | 2 +- matita/components/xml/dune | 2 +- matita/configure.ac | 2 +- matita/dune-project | 27 ++++++++++++++-------- matita/matita.opam | 29 +++++++++++++++--------- matita/matita/dune | 2 +- 25 files changed, 59 insertions(+), 43 deletions(-) diff --git a/matita/components/content/dune b/matita/components/content/dune index df473bb5b..bcaa09552 100644 --- a/matita/components/content/dune +++ b/matita/components/content/dune @@ -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)))) diff --git a/matita/components/content_pres/dune b/matita/components/content_pres/dune index bb9096176..c5f2c3923 100644 --- a/matita/components/content_pres/dune +++ b/matita/components/content_pres/dune @@ -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 :-( diff --git a/matita/components/disambiguation/dune b/matita/components/disambiguation/dune index 0b89f82dc..5f22ba2f2 100644 --- a/matita/components/disambiguation/dune +++ b/matita/components/disambiguation/dune @@ -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)))) diff --git a/matita/components/extlib/dune b/matita/components/extlib/dune index a81b6d646..83a3784e1 100644 --- a/matita/components/extlib/dune +++ b/matita/components/extlib/dune @@ -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)))) diff --git a/matita/components/getter/dune b/matita/components/getter/dune index 4356f0fe6..102e262ef 100644 --- a/matita/components/getter/dune +++ b/matita/components/getter/dune @@ -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)))) diff --git a/matita/components/grafite/dune b/matita/components/grafite/dune index 7deeb70be..41550f188 100644 --- a/matita/components/grafite/dune +++ b/matita/components/grafite/dune @@ -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)))) diff --git a/matita/components/grafite_engine/dune b/matita/components/grafite_engine/dune index a40b33794..5370981e9 100644 --- a/matita/components/grafite_engine/dune +++ b/matita/components/grafite_engine/dune @@ -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)))) diff --git a/matita/components/grafite_parser/dune b/matita/components/grafite_parser/dune index 329efec92..22aa2475b 100644 --- a/matita/components/grafite_parser/dune +++ b/matita/components/grafite_parser/dune @@ -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 :-( diff --git a/matita/components/library/dune b/matita/components/library/dune index cf880522f..47c9d3071 100644 --- a/matita/components/library/dune +++ b/matita/components/library/dune @@ -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)))) diff --git a/matita/components/logger/dune b/matita/components/logger/dune index 4313f42a4..029fb06bd 100644 --- a/matita/components/logger/dune +++ b/matita/components/logger/dune @@ -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)))) diff --git a/matita/components/ng_cic_content/dune b/matita/components/ng_cic_content/dune index 66853b1e1..ed7eb41a7 100644 --- a/matita/components/ng_cic_content/dune +++ b/matita/components/ng_cic_content/dune @@ -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)))) diff --git a/matita/components/ng_disambiguation/dune b/matita/components/ng_disambiguation/dune index dd7b556ce..2ff739a9c 100644 --- a/matita/components/ng_disambiguation/dune +++ b/matita/components/ng_disambiguation/dune @@ -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)))) diff --git a/matita/components/ng_extraction/dune b/matita/components/ng_extraction/dune index 92f7d14f2..af7246769 100644 --- a/matita/components/ng_extraction/dune +++ b/matita/components/ng_extraction/dune @@ -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)))) diff --git a/matita/components/ng_kernel/dune b/matita/components/ng_kernel/dune index 4bd483ca8..c0564318e 100644 --- a/matita/components/ng_kernel/dune +++ b/matita/components/ng_kernel/dune @@ -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)))) diff --git a/matita/components/ng_library/dune b/matita/components/ng_library/dune index efb88ef68..bc4fe3bce 100644 --- a/matita/components/ng_library/dune +++ b/matita/components/ng_library/dune @@ -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)))) diff --git a/matita/components/ng_paramodulation/dune b/matita/components/ng_paramodulation/dune index be0a28530..cf0544396 100644 --- a/matita/components/ng_paramodulation/dune +++ b/matita/components/ng_paramodulation/dune @@ -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)))) diff --git a/matita/components/ng_refiner/dune b/matita/components/ng_refiner/dune index 72b3f7b4a..cb6b5688a 100644 --- a/matita/components/ng_refiner/dune +++ b/matita/components/ng_refiner/dune @@ -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)))) diff --git a/matita/components/ng_tactics/dune b/matita/components/ng_tactics/dune index 473674ab2..b2d38160f 100644 --- a/matita/components/ng_tactics/dune +++ b/matita/components/ng_tactics/dune @@ -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)))) diff --git a/matita/components/registry/dune b/matita/components/registry/dune index 15b3173b7..10dcf8188 100644 --- a/matita/components/registry/dune +++ b/matita/components/registry/dune @@ -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)))) diff --git a/matita/components/syntax_extensions/dune b/matita/components/syntax_extensions/dune index c780ece7f..e7d02a81c 100644 --- a/matita/components/syntax_extensions/dune +++ b/matita/components/syntax_extensions/dune @@ -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)))) diff --git a/matita/components/xml/dune b/matita/components/xml/dune index fb60d63c6..ba113bd70 100644 --- a/matita/components/xml/dune +++ b/matita/components/xml/dune @@ -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)))) diff --git a/matita/configure.ac b/matita/configure.ac index ba25fab4d..cf8a8e4ee 100644 --- a/matita/configure.ac +++ b/matita/configure.ac @@ -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 diff --git a/matita/dune-project b/matita/dune-project index 99912ea13..4dbce59a9 100644 --- a/matita/dune-project +++ b/matita/dune-project @@ -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 diff --git a/matita/matita.opam b/matita/matita.opam index 5e02c0e59..bba4c6547 100644 --- a/matita/matita.opam +++ b/matita/matita.opam @@ -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" diff --git a/matita/matita/dune b/matita/matita/dune index 3a59004f7..1c87a7269 100644 --- a/matita/matita/dune +++ b/matita/matita/dune @@ -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 -- 2.39.2