Preliminary support for dune

- dune build matita/matita{,c,clean}.exe works
- dune build fails on components/syntax_extensions where we need
  to add modules to two different libraries. I have found a
  workaround (dune does not allow it!) that works when building
  matita*.exe, but not when doing "dune build"
- the dune files and the Makefiles are not 100% equivalent
  (e.g. some modules not dropped during compilation, the user
  interface not generated by glade yet)

diff --git a/matita/components/content/dune b/matita/components/content/dune
new file mode 100644 (file)
index 0000000..df473bb
--- /dev/null
+++ b/matita/components/content/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_content)
+ (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
new file mode 100644 (file)
index 0000000..4ff7cd7
--- /dev/null
+++ b/matita/components/content_pres/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_content_pres)
+ (libraries helm_content helm_syntax_extensions camlp5.gramlib ulex-camlp5 helm_grafite)
+ (preprocess (action (system "camlp5o -I components/syntax_extensions -I `ocamlfind query ulex-camlp5` pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc %{input-file}")))
+ (preprocessor_deps ../syntax_extensions/pa_unicode_macro.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
new file mode 100644 (file)
index 0000000..0b89f82
--- /dev/null
+++ b/matita/components/disambiguation/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_disambiguation)
+ (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
new file mode 100644 (file)
index 0000000..a81b6d6
--- /dev/null
+++ b/matita/components/extlib/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_extlib)
+ (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
new file mode 100644 (file)
index 0000000..4356f0f
--- /dev/null
+++ b/matita/components/getter/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_getter)
+ (libraries http unix pcre zip helm_xml helm_logger helm_ng_kernel helm_registry)
+ (preprocess (action (system "camlp5o %{input-file}")))
+ (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
new file mode 100644 (file)
index 0000000..7deeb70
--- /dev/null
+++ b/matita/components/grafite/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_grafite)
+ (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
new file mode 100644 (file)
index 0000000..a40b337
--- /dev/null
+++ b/matita/components/grafite_engine/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_grafite_engine)
+ (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
new file mode 100644 (file)
index 0000000..f9ba525
--- /dev/null
+++ b/matita/components/grafite_parser/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_grafite_parser)
+ (libraries helm_grafite ulex-camlp5 helm_ng_disambiguation helm_ng_library helm_content_pres)
+ (preprocess (action (system "camlp5o -I components/syntax_extensions -I `ocamlfind query ulex-camlp5` pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc %{input-file}")))
+ (preprocessor_deps ../syntax_extensions/pa_unicode_macro.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
new file mode 100644 (file)
index 0000000..cf88052
--- /dev/null
+++ b/matita/components/library/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_library)
+ (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
new file mode 100644 (file)
index 0000000..4313f42
--- /dev/null
+++ b/matita/components/logger/dune
@@ -0,0 +1,6 @@
+(library
+ (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
new file mode 100644 (file)
index 0000000..66853b1
--- /dev/null
+++ b/matita/components/ng_cic_content/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_ng_cic_content)
+ (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
new file mode 100644 (file)
index 0000000..dd7b556
--- /dev/null
+++ b/matita/components/ng_disambiguation/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_ng_disambiguation)
+ (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
new file mode 100644 (file)
index 0000000..92f7d14
--- /dev/null
+++ b/matita/components/ng_extraction/dune
@@ -0,0 +1,8 @@
+(library
+ (name helm_ng_extraction)
+ (libraries helm_ng_kernel helm_registry)
+ (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
new file mode 100644 (file)
index 0000000..4bd483c
--- /dev/null
+++ b/matita/components/ng_kernel/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_ng_kernel)
+ (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
new file mode 100644 (file)
index 0000000..efb88ef
--- /dev/null
+++ b/matita/components/ng_library/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_ng_library)
+ (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
new file mode 100644 (file)
index 0000000..be0a285
--- /dev/null
+++ b/matita/components/ng_paramodulation/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_ng_paramodulation)
+ (libraries helm_ng_refiner)
+ (wrapped false)
+ (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
new file mode 100644 (file)
index 0000000..72b3f7b
--- /dev/null
+++ b/matita/components/ng_refiner/dune
@@ -0,0 +1,8 @@
+(library
+ (name helm_ng_refiner)
+ (libraries helm_ng_kernel)
+ (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
new file mode 100644 (file)
index 0000000..473674a
--- /dev/null
+++ b/matita/components/ng_tactics/dune
@@ -0,0 +1,7 @@
+(library
+ (name helm_ng_tactics)
+ (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
new file mode 100644 (file)
index 0000000..15b3173
--- /dev/null
+++ b/matita/components/registry/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_registry)
+ (libraries str netstring helm_xml)
+ (preprocess (action (system "camlp5o %{input-file}")))
+ (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
new file mode 100644 (file)
index 0000000..884403e
--- /dev/null
+++ b/matita/components/syntax_extensions/dune
@@ -0,0 +1,36 @@
+(executable
+ (public_name make_table)
+ (name make_table)
+ (libraries helm_xml)
+ (modules make_table))
+
+(library
+ (name helm_syntax_extensions)
+ (libraries str)
+ (wrapped false)
+ (modules utf8Macro utf8MacroTable))
+
+(library
+ (name pa_unicode_macro)
+ (libraries camlp5 helm_syntax_extensions)
+ (wrapped false)
+ (preprocess (action (system "camlp5o q_MLast.cmo pa_extend.cmo -loc loc %{input-file}")))
+ (preprocessor_deps helm_syntax_extensions.cma)
+ (library_flags components/syntax_extensions/helm_syntax_extensions.cma)
+ (modules pa_unicode_macro))
+
+(library
+ (name profiling_macros)
+ (libraries str)
+ (wrapped false)
+ (modules profiling_macros))
+
+(rule
+ (targets utf8MacroTable.ml utf8MacroTable.ml.txt)
+ (deps (glob_files data/*.xml) make_table.exe)
+ (mode (promote))
+ (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
new file mode 100644 (file)
index 0000000..fb60d63
--- /dev/null
+++ b/matita/components/xml/dune
@@ -0,0 +1,9 @@
+(library
+ (name helm_xml)
+ (libraries zip expat helm_extlib camlp-streams)
+ (preprocess (action (system "camlp5o %{input-file}")))
+ (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/dune-project b/matita/dune-project
new file mode 100644 (file)
index 0000000..99912ea
--- /dev/null
+++ b/matita/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.6)
+
+(name matita)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name matita)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune)
+ (tags
+  (topics "to describe" your project)))
+
+; 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
new file mode 100644 (file)
index 0000000..5e02c0e
--- /dev/null
+++ b/matita/matita.opam
@@ -0,0 +1,31 @@
+# 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"
+depends: [
+  "ocaml"
+  "dune" {>= "3.6"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/username/reponame.git"

diff --git a/matita/matita/dune b/matita/matita/dune
new file mode 100644 (file)
index 0000000..3a59004
--- /dev/null
+++ b/matita/matita/dune
@@ -0,0 +1,26 @@
+(library
+ (name matita_cli)
+ (wrapped false)
+ (libraries helm_grafite_engine lablgtk3-sourceview3)
+ (modules 
+   buildTimeConf matitaTypes matitaMiscCli applyTransformation matitaEngine matitaExcPp matitaInit))
+
+(executable
+ (name matita)
+ (public_name matita)
+ (promote (until-clean))
+ (libraries matita_cli)
+ (modules_without_implementation matitaGuiTypes)
+ (modules
+   matitaGuiInit matitaGeneratedGui lablGraphviz matitaGuiTypes matitaMisc matitaGtkMisc virtuals cicMathView predefined_virtuals matitaMathView matitaScript matitaGui matita))
+
+(executables
+ (names matitac matitaclean)
+ (public_names matitac matitaclean)
+ (promote (until-clean)) 
+ (libraries matita_cli)
+ (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