(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))))
(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 :-(
(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))))
(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))))
(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))))
(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))))
(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))))
(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 :-(
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
(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))))
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
(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
# 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: [
"@doc" {with-doc}
]
]
-dev-repo: "git+https://github.com/username/reponame.git"
+dev-repo: "http://matita.cs.unibo.it/download.shtml"
(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