From 712af5b8dc7dab1ebfa6532b73b91c96cb4c6837 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Jan 2023 20:42:56 +0100 Subject: [PATCH] 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) --- matita/components/content/dune | 7 +++++ matita/components/content_pres/dune | 9 ++++++ matita/components/disambiguation/dune | 7 +++++ matita/components/extlib/dune | 7 +++++ matita/components/getter/dune | 9 ++++++ matita/components/grafite/dune | 7 +++++ matita/components/grafite_engine/dune | 7 +++++ matita/components/grafite_parser/dune | 9 ++++++ matita/components/library/dune | 7 +++++ matita/components/logger/dune | 6 ++++ matita/components/ng_cic_content/dune | 7 +++++ matita/components/ng_disambiguation/dune | 7 +++++ matita/components/ng_extraction/dune | 8 ++++++ matita/components/ng_kernel/dune | 7 +++++ matita/components/ng_library/dune | 7 +++++ matita/components/ng_paramodulation/dune | 9 ++++++ matita/components/ng_refiner/dune | 8 ++++++ matita/components/ng_tactics/dune | 7 +++++ matita/components/registry/dune | 9 ++++++ matita/components/syntax_extensions/dune | 36 ++++++++++++++++++++++++ matita/components/xml/dune | 9 ++++++ matita/dune-project | 26 +++++++++++++++++ matita/matita.opam | 31 ++++++++++++++++++++ matita/matita/dune | 26 +++++++++++++++++ 24 files changed, 272 insertions(+) create mode 100644 matita/components/content/dune create mode 100644 matita/components/content_pres/dune create mode 100644 matita/components/disambiguation/dune create mode 100644 matita/components/extlib/dune create mode 100644 matita/components/getter/dune create mode 100644 matita/components/grafite/dune create mode 100644 matita/components/grafite_engine/dune create mode 100644 matita/components/grafite_parser/dune create mode 100644 matita/components/library/dune create mode 100644 matita/components/logger/dune create mode 100644 matita/components/ng_cic_content/dune create mode 100644 matita/components/ng_disambiguation/dune create mode 100644 matita/components/ng_extraction/dune create mode 100644 matita/components/ng_kernel/dune create mode 100644 matita/components/ng_library/dune create mode 100644 matita/components/ng_paramodulation/dune create mode 100644 matita/components/ng_refiner/dune create mode 100644 matita/components/ng_tactics/dune create mode 100644 matita/components/registry/dune create mode 100644 matita/components/syntax_extensions/dune create mode 100644 matita/components/xml/dune create mode 100644 matita/dune-project create mode 100644 matita/matita.opam create mode 100644 matita/matita/dune diff --git a/matita/components/content/dune b/matita/components/content/dune new file mode 100644 index 000000000..df473bb5b --- /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 index 000000000..4ff7cd7a4 --- /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 index 000000000..0b89f82dc --- /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 index 000000000..a81b6d646 --- /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 index 000000000..4356f0fe6 --- /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 index 000000000..7deeb70be --- /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 index 000000000..a40b33794 --- /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 index 000000000..f9ba525bc --- /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 index 000000000..cf880522f --- /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 index 000000000..4313f42a4 --- /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 index 000000000..66853b1e1 --- /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 index 000000000..dd7b556ce --- /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 index 000000000..92f7d14f2 --- /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 index 000000000..4bd483ca8 --- /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 index 000000000..efb88ef68 --- /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 index 000000000..be0a28530 --- /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 index 000000000..72b3f7b4a --- /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 index 000000000..473674ab2 --- /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 index 000000000..15b3173b7 --- /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 index 000000000..884403ee6 --- /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 index 000000000..fb60d63c6 --- /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 index 000000000..99912ea13 --- /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 index 000000000..5e02c0e59 --- /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 index 000000000..3a59004f7 --- /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 -- 2.39.2