From 999a4d69eebec9e8bc8b8ad226403d2920d47d3c Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 5 Feb 2026 02:23:18 +0100 Subject: [PATCH 1/3] Switch from [coq.theory] to [rocq.theory]. --- apps/NES/elpi/dune | 2 +- apps/NES/examples/dune | 2 +- apps/NES/tests/dune | 2 +- apps/NES/theories/dune | 2 +- apps/coercion/src/dune | 4 ++-- apps/coercion/tests/dune | 2 +- apps/coercion/theories/dune | 2 +- apps/cs/src/dune | 4 ++-- apps/cs/tests/dune | 3 +-- apps/cs/theories/dune | 2 +- apps/derive/elpi/dune | 2 +- apps/derive/examples/dune | 2 +- apps/derive/tests-stdlib/dune | 2 +- apps/derive/tests/dune | 2 +- apps/derive/theories/dune | 2 +- apps/eltac/examples/dune | 2 +- apps/eltac/tests-stdlib/dune | 2 +- apps/eltac/tests/dune | 2 +- apps/eltac/theories/dune | 2 +- apps/json/examples/dune | 2 +- apps/json/src/dune | 2 +- apps/json/tests-plugin/dune | 2 +- apps/json/theories/dune | 2 +- apps/locker/elpi/dune | 2 +- apps/locker/tests/dune | 2 +- apps/locker/theories/dune | 2 +- apps/rbuild/elpi/dune | 2 +- apps/rbuild/examples/dune | 2 +- apps/rbuild/theories/dune | 2 +- apps/tc/elpi/dune | 2 +- apps/tc/examples/dune | 2 +- apps/tc/src/dune | 4 ++-- apps/tc/tests-stdlib/dune | 2 +- apps/tc/tests/dune | 2 +- apps/tc/theories/dune | 2 +- apps/xml/examples/dune | 2 +- apps/xml/src/dune | 2 +- apps/xml/tests-plugin/dune | 2 +- apps/xml/theories/dune | 2 +- coq-elpi.opam | 19 ------------------- dune | 2 +- dune-project | 12 ++---------- elpi/dune | 2 +- examples-stdlib/dune | 2 +- examples/dune | 2 +- examples/example_plugin/dune-project | 4 ++-- examples/example_plugin/elpi/dune | 4 ++-- examples/example_plugin/tests/dune | 4 ++-- examples/example_plugin/theories/dune | 4 ++-- src/dune | 4 ++-- tests-stdlib/dune | 2 +- tests/dune | 4 ++-- theories/dune | 4 ++-- 53 files changed, 63 insertions(+), 91 deletions(-) delete mode 100644 coq-elpi.opam diff --git a/apps/NES/elpi/dune b/apps/NES/elpi/dune index 096a65a85..4525927d2 100644 --- a/apps/NES/elpi/dune +++ b/apps/NES/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.NES.elpi) (package rocq-elpi) (theories elpi)) diff --git a/apps/NES/examples/dune b/apps/NES/examples/dune index a71cea916..1221700c0 100644 --- a/apps/NES/examples/dune +++ b/apps/NES/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.NES.examples) (theories elpi elpi.apps.NES)) diff --git a/apps/NES/tests/dune b/apps/NES/tests/dune index d2ab3b5bd..3d9d40e2e 100644 --- a/apps/NES/tests/dune +++ b/apps/NES/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.NES.tests) (package rocq-elpi-tests) (theories elpi elpi.apps.NES)) diff --git a/apps/NES/theories/dune b/apps/NES/theories/dune index 33950b493..6e24beef3 100644 --- a/apps/NES/theories/dune +++ b/apps/NES/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.NES) (package rocq-elpi) (theories elpi elpi.apps.NES.elpi)) diff --git a/apps/coercion/src/dune b/apps/coercion/src/dune index 9f6ecf147..320acf703 100644 --- a/apps/coercion/src/dune +++ b/apps/coercion/src/dune @@ -2,8 +2,8 @@ (name elpi_coercion_plugin) (public_name rocq-elpi.coercion) (flags :standard -w -27) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi)) -(coq.pp +(rocq.pp (modules rocq_elpi_coercion_hook)) diff --git a/apps/coercion/tests/dune b/apps/coercion/tests/dune index 5d9965570..cc5935274 100644 --- a/apps/coercion/tests/dune +++ b/apps/coercion/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.coercion.tests) (package rocq-elpi-tests) (theories elpi elpi.apps.coercion)) diff --git a/apps/coercion/theories/dune b/apps/coercion/theories/dune index a4cb29733..64c11198a 100644 --- a/apps/coercion/theories/dune +++ b/apps/coercion/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.coercion) (package rocq-elpi) (theories elpi) diff --git a/apps/cs/src/dune b/apps/cs/src/dune index 594dd7861..4d2b7ba93 100644 --- a/apps/cs/src/dune +++ b/apps/cs/src/dune @@ -2,8 +2,8 @@ (name elpi_cs_plugin) (public_name rocq-elpi.cs) (flags :standard -w -27) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi)) -(coq.pp +(rocq.pp (modules rocq_elpi_cs_hook)) diff --git a/apps/cs/tests/dune b/apps/cs/tests/dune index 511463202..93035ba9e 100644 --- a/apps/cs/tests/dune +++ b/apps/cs/tests/dune @@ -1,7 +1,6 @@ (cram (applies_to :whole_subtree) (deps - %{bin:coqc} - %{bin:coqdep} + %{bin:rocq} (package rocq-elpi) setup-project.sh)) diff --git a/apps/cs/theories/dune b/apps/cs/theories/dune index 608660970..2c8b64642 100644 --- a/apps/cs/theories/dune +++ b/apps/cs/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.cs) (package rocq-elpi) (theories elpi) diff --git a/apps/derive/elpi/dune b/apps/derive/elpi/dune index 6db189007..47b8b0df0 100644 --- a/apps/derive/elpi/dune +++ b/apps/derive/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.derive.elpi) (package rocq-elpi) (theories elpi)) diff --git a/apps/derive/examples/dune b/apps/derive/examples/dune index 89e7e401a..4bde1b1ea 100644 --- a/apps/derive/examples/dune +++ b/apps/derive/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.derive.examples) (theories elpi elpi.apps.derive)) diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune index 147d5c92c..d31bbe7f3 100644 --- a/apps/derive/tests-stdlib/dune +++ b/apps/derive/tests-stdlib/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi-tests-stdlib) (name elpi_apps_derive_tests_stdlib) (flags :standard -w -default-output-directory) diff --git a/apps/derive/tests/dune b/apps/derive/tests/dune index a06ce33d5..2071a6512 100644 --- a/apps/derive/tests/dune +++ b/apps/derive/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.derive.tests) (package rocq-elpi-tests) (flags :standard -w -default-output-directory) diff --git a/apps/derive/theories/dune b/apps/derive/theories/dune index eb7cd2d6b..82dde71f9 100644 --- a/apps/derive/theories/dune +++ b/apps/derive/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.derive) (package rocq-elpi) (theories elpi elpi.apps.derive.elpi)) diff --git a/apps/eltac/examples/dune b/apps/eltac/examples/dune index 99eac545f..d9b7b2f24 100644 --- a/apps/eltac/examples/dune +++ b/apps/eltac/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.eltac.examples) (theories elpi elpi.apps.eltac)) diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune index 73a8c7cfb..8eeb60080 100644 --- a/apps/eltac/tests-stdlib/dune +++ b/apps/eltac/tests-stdlib/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi-tests-stdlib) (name elpi_apps_eltac_tests_stdlib) (theories elpi elpi.apps.eltac Stdlib)) diff --git a/apps/eltac/tests/dune b/apps/eltac/tests/dune index dde8292cc..a87b8b41b 100644 --- a/apps/eltac/tests/dune +++ b/apps/eltac/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.eltac.tests) (package rocq-elpi-tests) (theories elpi elpi.apps.eltac)) diff --git a/apps/eltac/theories/dune b/apps/eltac/theories/dune index 0a91ec7b6..e3108a454 100644 --- a/apps/eltac/theories/dune +++ b/apps/eltac/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.eltac) (package rocq-elpi) (theories elpi elpi.apps.derive)) diff --git a/apps/json/examples/dune b/apps/json/examples/dune index 88630f356..cdee6ed28 100644 --- a/apps/json/examples/dune +++ b/apps/json/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.json.examples) (theories elpi elpi.json elpi.json.tests)) diff --git a/apps/json/src/dune b/apps/json/src/dune index 27d3d7b95..1ed0ba324 100644 --- a/apps/json/src/dune +++ b/apps/json/src/dune @@ -2,5 +2,5 @@ (name elpi_json_plugin) (public_name rocq-elpi-json.elpi_json_plugin) (flags :standard -w -27) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi elpi yojson)) diff --git a/apps/json/tests-plugin/dune b/apps/json/tests-plugin/dune index bf417fe1a..0542035e6 100644 --- a/apps/json/tests-plugin/dune +++ b/apps/json/tests-plugin/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.json.tests) (package rocq-elpi-json-tests) (theories elpi elpi.json)) diff --git a/apps/json/theories/dune b/apps/json/theories/dune index abe0ad2b8..e5264dab3 100644 --- a/apps/json/theories/dune +++ b/apps/json/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.json) (theories elpi_elpi elpi) (plugins rocq-elpi-json.elpi_json_plugin) diff --git a/apps/locker/elpi/dune b/apps/locker/elpi/dune index 000dc366f..c2bdbf258 100644 --- a/apps/locker/elpi/dune +++ b/apps/locker/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.locker.elpi) (package rocq-elpi) (theories elpi)) diff --git a/apps/locker/tests/dune b/apps/locker/tests/dune index cadbe6376..4ca185a48 100644 --- a/apps/locker/tests/dune +++ b/apps/locker/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.locker.tests) (package rocq-elpi-tests) (theories elpi elpi.apps.locker)) diff --git a/apps/locker/theories/dune b/apps/locker/theories/dune index 35024b5a8..0af01f2ae 100644 --- a/apps/locker/theories/dune +++ b/apps/locker/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.locker) (package rocq-elpi) (theories elpi elpi.apps.locker.elpi)) diff --git a/apps/rbuild/elpi/dune b/apps/rbuild/elpi/dune index 04b2563e2..af8ff66ec 100644 --- a/apps/rbuild/elpi/dune +++ b/apps/rbuild/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.rbuild.elpi) (package rocq-elpi) (theories elpi elpi.apps.coercion)) diff --git a/apps/rbuild/examples/dune b/apps/rbuild/examples/dune index db00efcaa..e5610a4e6 100644 --- a/apps/rbuild/examples/dune +++ b/apps/rbuild/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.rbuild.examples) (theories elpi elpi.apps.rbuild elpi.apps.derive)) diff --git a/apps/rbuild/theories/dune b/apps/rbuild/theories/dune index 8a77f0712..7f8a16bd1 100644 --- a/apps/rbuild/theories/dune +++ b/apps/rbuild/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.rbuild) (package rocq-elpi) (theories elpi elpi.apps.rbuild.elpi elpi.apps.derive)) diff --git a/apps/tc/elpi/dune b/apps/tc/elpi/dune index 834876548..8133f9d88 100644 --- a/apps/tc/elpi/dune +++ b/apps/tc/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.tc.elpi) (package rocq-elpi) (theories elpi)) diff --git a/apps/tc/examples/dune b/apps/tc/examples/dune index 9cd85983e..7deeb8084 100644 --- a/apps/tc/examples/dune +++ b/apps/tc/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.tc.examples) (theories elpi elpi.apps.tc Stdlib)) diff --git a/apps/tc/src/dune b/apps/tc/src/dune index 6c60a9c10..562a8d429 100644 --- a/apps/tc/src/dune +++ b/apps/tc/src/dune @@ -2,8 +2,8 @@ (name elpi_tc_plugin) (public_name rocq-elpi.tc) (flags :standard -w -27) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi)) -(coq.pp +(rocq.pp (modules rocq_elpi_tc_hook)) diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune index fb351e464..cc8497ee5 100644 --- a/apps/tc/tests-stdlib/dune +++ b/apps/tc/tests-stdlib/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi-tests-stdlib) (name elpi_apps_tc_tests_stdlib) (flags :standard -async-proofs-cache force) diff --git a/apps/tc/tests/dune b/apps/tc/tests/dune index aa17dd497..9f472d8f7 100644 --- a/apps/tc/tests/dune +++ b/apps/tc/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.tc.tests) (flags :standard -async-proofs-cache force) (package rocq-elpi-tests) diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune index 6e7a83821..2263bb9ea 100644 --- a/apps/tc/theories/dune +++ b/apps/tc/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.apps.tc) (package rocq-elpi) (theories elpi elpi.apps.tc.elpi) diff --git a/apps/xml/examples/dune b/apps/xml/examples/dune index a82cb7720..921cef7a3 100644 --- a/apps/xml/examples/dune +++ b/apps/xml/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.xml.examples) (theories elpi elpi.xml elpi.xml.tests)) diff --git a/apps/xml/src/dune b/apps/xml/src/dune index c381d6298..47661aa3e 100644 --- a/apps/xml/src/dune +++ b/apps/xml/src/dune @@ -2,5 +2,5 @@ (name elpi_xml_plugin) (public_name rocq-elpi-xml.elpi_xml_plugin) (flags :standard -w -27) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi elpi xml-light)) diff --git a/apps/xml/tests-plugin/dune b/apps/xml/tests-plugin/dune index c85f41de6..95deeca57 100644 --- a/apps/xml/tests-plugin/dune +++ b/apps/xml/tests-plugin/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.xml.tests) (package rocq-elpi-xml-tests) (theories elpi elpi.xml)) diff --git a/apps/xml/theories/dune b/apps/xml/theories/dune index 314e91ca8..c2560776f 100644 --- a/apps/xml/theories/dune +++ b/apps/xml/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.xml) (theories elpi_elpi elpi) (plugins rocq-elpi-xml.elpi_xml_plugin) diff --git a/coq-elpi.opam b/coq-elpi.opam deleted file mode 100644 index c80409da4..000000000 --- a/coq-elpi.opam +++ /dev/null @@ -1,19 +0,0 @@ -# This file is generated by dune, edit dune-project instead -opam-version: "2.0" -synopsis: "Compatibility metapackage for Elpi extension language after the Rocq renaming" -maintainer: ["Enrico Tassi "] -authors: ["Enrico Tassi "] -license: "LGPL-2.1-or-later" -tags: [ - "category:Miscellaneous/Coq Extensions" - "keyword:λProlog" - "keyword:higher order abstract syntax" - "logpath:elpi" -] -homepage: "https://github.com/LPCIC/coq-elpi" -bug-reports: "https://github.com/LPCIC/coq-elpi/issues" -depends: [ - "coq-core" - "rocq-elpi" {= version} -] -dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" diff --git a/dune b/dune index 85555381b..5bae1b06b 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ (env (dev (flags (:standard -w -9 -w -32 -w -27 -w -6 -w -37 -warn-error -A)) - (coq (flags -w -register-all -w -notation-for-abbreviation -w +elpi.deprecated -w +elpi.implication-precedence -w -elpi.flex-clause -w +elpi.missing-types -bt)))) + (rocq (flags -w -register-all -w -notation-for-abbreviation -w +elpi.deprecated -w +elpi.implication-precedence -w -elpi.flex-clause -w +elpi.missing-types -bt)))) diff --git a/dune-project b/dune-project index a71a5bd67..4a9c0e82b 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ -(lang dune 3.13) -(using coq 0.8) +(lang dune 3.21) +(using rocq 0.11) (name rocq-elpi) ;(generate_opam_files) @@ -70,11 +70,3 @@ (synopsis "Technical package to run tests depending on Stdlib") (description "Do not install") (depends rocq-elpi rocq-stdlib)) - -(package - (name coq-elpi) - (allow_empty) - (depends - coq-core - (rocq-elpi (= :version))) - (synopsis "Compatibility metapackage for Elpi extension language after the Rocq renaming")) diff --git a/elpi/dune b/elpi/dune index cf2ad65a6..bf1b33f29 100644 --- a/elpi/dune +++ b/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi_elpi) ; FIXME (package rocq-elpi)) diff --git a/examples-stdlib/dune b/examples-stdlib/dune index ec9aa161b..f0103f21f 100644 --- a/examples-stdlib/dune +++ b/examples-stdlib/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi-tests-stdlib) (name elpi_examples_stdlib) (plugins rocq-elpi.elpi) diff --git a/examples/dune b/examples/dune index 42fc8f5c7..62d3ddf7d 100644 --- a/examples/dune +++ b/examples/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi) (name elpi_examples) (plugins rocq-elpi.elpi) diff --git a/examples/example_plugin/dune-project b/examples/example_plugin/dune-project index f365b8699..7f9c10228 100644 --- a/examples/example_plugin/dune-project +++ b/examples/example_plugin/dune-project @@ -1,5 +1,5 @@ -(lang dune 3.13) -(using coq 0.8) +(lang dune 3.21) +(using rocq 0.11) (name Ext) (generate_opam_files true) diff --git a/examples/example_plugin/elpi/dune b/examples/example_plugin/elpi/dune index c56dab36b..0dc0ba6c7 100644 --- a/examples/example_plugin/elpi/dune +++ b/examples/example_plugin/elpi/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory ; myExtension.lib is the logical path that can be used in rocq (name myExtension.lib) (theories elpi) @@ -17,4 +17,4 @@ (action (with-stdout-to %{target} (progn - (run rocq_elpi_shafile %{deps}))))) \ No newline at end of file + (run rocq_elpi_shafile %{deps}))))) diff --git a/examples/example_plugin/tests/dune b/examples/example_plugin/tests/dune index 46e5d761c..71af3e6dc 100644 --- a/examples/example_plugin/tests/dune +++ b/examples/example_plugin/tests/dune @@ -1,7 +1,7 @@ -(coq.theory +(rocq.theory (name myExtension.tests) (package myExtension-tests) ; the tests folder depends on ext (theories elpi_elpi elpi myExtension myExtension.lib)) -(include_subdirs qualified) \ No newline at end of file +(include_subdirs qualified) diff --git a/examples/example_plugin/theories/dune b/examples/example_plugin/theories/dune index fac7d89dc..2d7cdee95 100644 --- a/examples/example_plugin/theories/dune +++ b/examples/example_plugin/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory ; myExtension is the logical path that can be used in rocq to import the ; the .v in the theories folder (name myExtension) @@ -10,4 +10,4 @@ (plugins myExtension.plugin) (package myExtension)) -(include_subdirs qualified) \ No newline at end of file +(include_subdirs qualified) diff --git a/src/dune b/src/dune index 1376f7141..c4d1ca097 100644 --- a/src/dune +++ b/src/dune @@ -5,7 +5,7 @@ (flags :standard -w -27) (preprocessor_deps rocq_elpi_config.mlh) (preprocess - (pps ppx_deriving.std ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (pps ppx_deriving.std ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{rocq:version.major}.%{rocq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac elpi)) (rule @@ -46,5 +46,5 @@ (echo "]\n"))))) -(coq.pp +(rocq.pp (modules rocq_elpi_vernacular_syntax rocq_elpi_arg_syntax)) diff --git a/tests-stdlib/dune b/tests-stdlib/dune index 00c0b019b..5aec0e173 100644 --- a/tests-stdlib/dune +++ b/tests-stdlib/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (package rocq-elpi-tests-stdlib) (name elpi_tests_stdlib) (plugins rocq-elpi.elpi) diff --git a/tests/dune b/tests/dune index 9317ab5a7..31c2a8b43 100644 --- a/tests/dune +++ b/tests/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi.tests) (plugins rocq-elpi.elpi) (theories elpi)) @@ -11,7 +11,7 @@ (glob_files test_API_proof.v.in)) (action (with-stdout-to %{target} - (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{rocq:version.major}.%{rocq:version.minor}" %{deps})))) (rule (target dummy.v) diff --git a/theories/dune b/theories/dune index 7a1e22cfe..99d12482d 100644 --- a/theories/dune +++ b/theories/dune @@ -1,4 +1,4 @@ -(coq.theory +(rocq.theory (name elpi) (package rocq-elpi) (plugins rocq-elpi.elpi) @@ -10,6 +10,6 @@ (glob_files elpi.v.in)) (action (with-stdout-to %{target} - (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{rocq:version.major}.%{rocq:version.minor}" %{deps})))) (include_subdirs qualified) From 544d1b37b2911b18ce771ae54e2efa841e3ec68a Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 10 Jun 2026 21:32:10 +0200 Subject: [PATCH 2/3] Generate [_RocqProject] files with [dune]. --- .gitignore | 4 +- _CoqProject | 93 --------------------------- apps/NES/elpi/dune | 1 + apps/NES/examples/dune | 1 + apps/NES/tests/dune | 1 + apps/NES/theories/dune | 1 + apps/coercion/tests/dune | 1 + apps/coercion/theories/dune | 1 + apps/cs/theories/dune | 1 + apps/derive/elpi/dune | 1 + apps/derive/examples/dune | 1 + apps/derive/tests-stdlib/dune | 3 +- apps/derive/tests/dune | 1 + apps/derive/theories/dune | 1 + apps/eltac/examples/dune | 1 + apps/eltac/tests-stdlib/dune | 3 +- apps/eltac/tests/dune | 1 + apps/eltac/theories/dune | 1 + apps/json/examples/dune | 1 + apps/json/tests-plugin/dune | 3 +- apps/json/theories/dune | 1 + apps/locker/elpi/dune | 1 + apps/locker/tests/dune | 1 + apps/locker/theories/dune | 1 + apps/rbuild/elpi/dune | 1 + apps/rbuild/examples/dune | 1 + apps/rbuild/theories/dune | 1 + apps/tc/elpi/dune | 1 + apps/tc/examples/dune | 1 + apps/tc/tests-stdlib/dune | 3 +- apps/tc/tests/dune | 3 +- apps/tc/theories/dune | 3 +- apps/xml/examples/dune | 1 + apps/xml/tests-plugin/dune | 3 +- apps/xml/theories/dune | 5 +- elpi/dune | 3 +- examples-stdlib/dune | 3 +- examples/dune | 3 +- examples/example_plugin/elpi/dune | 1 + examples/example_plugin/tests/dune | 1 + examples/example_plugin/theories/dune | 2 + tests-stdlib/dune | 3 +- tests/dune | 1 + theories/dune | 1 + 44 files changed, 59 insertions(+), 107 deletions(-) delete mode 100644 _CoqProject diff --git a/.gitignore b/.gitignore index 2e4af63d4..85686866c 100644 --- a/.gitignore +++ b/.gitignore @@ -62,4 +62,6 @@ theories-stdlib/dune apps/coercion/src/dune apps/cs/src/dune apps/tc/src/dune -src/dune \ No newline at end of file +src/dune + +_RocqProject diff --git a/_CoqProject b/_CoqProject deleted file mode 100644 index eadb2ecb0..000000000 --- a/_CoqProject +++ /dev/null @@ -1,93 +0,0 @@ --arg -w -arg +elpi.deprecated --arg -w -arg -ambiguous-extra-dep --arg -w -arg -future-coercion-class-field - -# Plugins. - --I _build/install/default/lib - -# Theories - --R theories elpi --R _build/default/theories elpi - --Q elpi elpi_elpi --Q _build/default/elpi elpi_elpi - --Q examples elpi.examples --Q _build/default/examples elpi.examples --Q examples-stdlib elpi_examples_stdlib --Q _build/default/examples-stdlib elpi_examples_stdlib - --Q apps/coercion/tests elpi.apps.coercion.tests --Q _build/default/apps/coercion/tests elpi.apps.coercion.tests --Q apps/coercion/theories elpi.apps.coercion --Q _build/default/apps/coercion/theories elpi.apps.coercion --Q apps/cs/tests elpi.apps.cs.tests --Q _build/default/apps/cs/tests elpi.apps.cs.tests --Q apps/cs/theories elpi.apps.cs --Q _build/default/apps/cs/theories elpi.apps.cs - --Q apps/derive/elpi elpi.apps.derive.elpi --Q _build/default/apps/derive/elpi elpi.apps.derive.elpi --Q apps/derive/examples elpi.apps.derive.examples --Q _build/default/apps/derive/examples elpi.apps.derive.examples --Q apps/derive/theories elpi.apps.derive --Q _build/default/apps/derive/theories elpi.apps.derive --Q apps/derive/theories/derive elpi.apps.derive.derive --Q _build/default/apps/derive/theories/derive elpi.apps.derive.derive - --Q _build/default/apps/derive/tests elpi.apps.derive.tests --Q apps/derive/tests-stdlib elpi_apps_derive_tests_stdlib --Q _build/default/apps/derive/tests-stdlib elpi_apps_derive_tests_stdlib - --Q apps/eltac/examples elpi.apps.eltac.examples --Q _build/default/apps/eltac/examples elpi.apps.eltac.examples --Q apps/eltac/theories elpi.apps.eltac --Q _build/default/apps/eltac/theories elpi.apps.eltac --Q apps/eltac/tests elpi.apps.eltac.tests --Q _build/default/apps/eltac/tests elpi.apps.eltac.tests --Q apps/eltac/tests-stdlib elpi_apps_eltac_tests_stdlib --Q _build/default/apps/eltac/tests-stdlib elpi_apps_eltac_tests_stdlib - --Q apps/locker/elpi elpi.apps.locker.elpi --Q _build/default/apps/locker/elpi elpi.apps.locker.elpi --Q apps/locker/tests elpi.apps.locker.tests --Q _build/default/apps/locker/tests elpi.apps.locker.tests --Q apps/locker/theories elpi.apps.locker --Q _build/default/apps/locker/theories elpi.apps.locker - --Q apps/NES/elpi elpi.apps.NES.elpi --Q _build/default/apps/NES/elpi elpi.apps.NES.elpi --Q apps/NES/examples elpi.apps.NES.examples --Q _build/default/apps/NES/examples elpi.apps.NES.examples --Q apps/NES/tests elpi.apps.NES.tests --Q _build/default/apps/NES/tests elpi.apps.NES.tests --Q apps/NES/theories elpi.apps.NES --Q _build/default/apps/NES/theories elpi.apps.NES - --Q apps/tc/elpi elpi.apps.tc.elpi --Q _build/default/apps/tc/elpi elpi.apps.tc.elpi --Q apps/tc/examples elpi.apps.tc.examples --Q _build/default/apps/tc/examples elpi.apps.tc.examples --Q apps/tc/theories elpi.apps.tc --Q _build/default/apps/tc/theories elpi.apps.tc --Q _build/default/apps/tc/tests elpi.apps.tc.tests --Q apps/tc/tests elpi.apps.tc.tests --Q _build/default/apps/tc/tests-stdlib elpi_apps_tc_tests_stdlib --Q apps/tc/tests-stdlib elpi_apps_tc_tests_stdlib - --Q apps/rbuild/elpi elpi.apps.rbuild.elpi --Q _build/default/apps/rbuild/elpi elpi.apps.rbuild.elpi --Q apps/rbuild/examples elpi.apps.rbuild.examples --Q _build/default/apps/rbuild/examples elpi.apps.rbuild.examples --Q apps/rbuild/theories elpi.apps.rbuild --Q _build/default/apps/rbuild/theories elpi.apps.rbuild - -# Cram tests. - --Q tests elpi.tests --Q _build/default/tests elpi.tests - --Q tests-stdlib elpi_tests_stdlib --Q _build/default/tests-stdlib elpi_tests_stdlib diff --git a/apps/NES/elpi/dune b/apps/NES/elpi/dune index 4525927d2..2a3519b0c 100644 --- a/apps/NES/elpi/dune +++ b/apps/NES/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.NES.elpi) (package rocq-elpi) + (generate_project_file) (theories elpi)) (rule diff --git a/apps/NES/examples/dune b/apps/NES/examples/dune index 1221700c0..b823c3021 100644 --- a/apps/NES/examples/dune +++ b/apps/NES/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.apps.NES.examples) + (generate_project_file) (theories elpi elpi.apps.NES)) (include_subdirs qualified) diff --git a/apps/NES/tests/dune b/apps/NES/tests/dune index 3d9d40e2e..7f68cbe3d 100644 --- a/apps/NES/tests/dune +++ b/apps/NES/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.NES.tests) (package rocq-elpi-tests) + (generate_project_file) (theories elpi elpi.apps.NES)) (include_subdirs qualified) diff --git a/apps/NES/theories/dune b/apps/NES/theories/dune index 6e24beef3..7381e0da5 100644 --- a/apps/NES/theories/dune +++ b/apps/NES/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.NES) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.NES.elpi)) (include_subdirs qualified) diff --git a/apps/coercion/tests/dune b/apps/coercion/tests/dune index cc5935274..8b467b767 100644 --- a/apps/coercion/tests/dune +++ b/apps/coercion/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.coercion.tests) (package rocq-elpi-tests) + (generate_project_file) (theories elpi elpi.apps.coercion)) (include_subdirs qualified) diff --git a/apps/coercion/theories/dune b/apps/coercion/theories/dune index 64c11198a..0c1459843 100644 --- a/apps/coercion/theories/dune +++ b/apps/coercion/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.coercion) (package rocq-elpi) + (generate_project_file) (theories elpi) (plugins rocq-elpi.coercion)) diff --git a/apps/cs/theories/dune b/apps/cs/theories/dune index 2c8b64642..a46b90b5e 100644 --- a/apps/cs/theories/dune +++ b/apps/cs/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.cs) (package rocq-elpi) + (generate_project_file) (theories elpi) (plugins rocq-elpi.cs)) diff --git a/apps/derive/elpi/dune b/apps/derive/elpi/dune index 47b8b0df0..dc383922c 100644 --- a/apps/derive/elpi/dune +++ b/apps/derive/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.derive.elpi) (package rocq-elpi) + (generate_project_file) (theories elpi)) (rule diff --git a/apps/derive/examples/dune b/apps/derive/examples/dune index 4bde1b1ea..f799d6f6a 100644 --- a/apps/derive/examples/dune +++ b/apps/derive/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.apps.derive.examples) + (generate_project_file) (theories elpi elpi.apps.derive)) (include_subdirs qualified) diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune index d31bbe7f3..141ca6410 100644 --- a/apps/derive/tests-stdlib/dune +++ b/apps/derive/tests-stdlib/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi-tests-stdlib) (name elpi_apps_derive_tests_stdlib) + (package rocq-elpi-tests-stdlib) + (generate_project_file) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive elpi.apps.derive.tests Stdlib)) diff --git a/apps/derive/tests/dune b/apps/derive/tests/dune index 2071a6512..678b202c9 100644 --- a/apps/derive/tests/dune +++ b/apps/derive/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.derive.tests) (package rocq-elpi-tests) + (generate_project_file) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive)) diff --git a/apps/derive/theories/dune b/apps/derive/theories/dune index 82dde71f9..c6bf039a7 100644 --- a/apps/derive/theories/dune +++ b/apps/derive/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.derive) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.derive.elpi)) (include_subdirs qualified) diff --git a/apps/eltac/examples/dune b/apps/eltac/examples/dune index d9b7b2f24..77006bd13 100644 --- a/apps/eltac/examples/dune +++ b/apps/eltac/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.apps.eltac.examples) + (generate_project_file) (theories elpi elpi.apps.eltac)) (include_subdirs qualified) diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune index 8eeb60080..6b9679168 100644 --- a/apps/eltac/tests-stdlib/dune +++ b/apps/eltac/tests-stdlib/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi-tests-stdlib) (name elpi_apps_eltac_tests_stdlib) + (package rocq-elpi-tests-stdlib) + (generate_project_file) (theories elpi elpi.apps.eltac Stdlib)) (include_subdirs qualified) diff --git a/apps/eltac/tests/dune b/apps/eltac/tests/dune index a87b8b41b..c632ef75d 100644 --- a/apps/eltac/tests/dune +++ b/apps/eltac/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.eltac.tests) (package rocq-elpi-tests) + (generate_project_file) (theories elpi elpi.apps.eltac)) (include_subdirs qualified) diff --git a/apps/eltac/theories/dune b/apps/eltac/theories/dune index e3108a454..e425b9122 100644 --- a/apps/eltac/theories/dune +++ b/apps/eltac/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.eltac) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.derive)) (include_subdirs qualified) diff --git a/apps/json/examples/dune b/apps/json/examples/dune index cdee6ed28..65508a2ac 100644 --- a/apps/json/examples/dune +++ b/apps/json/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.json.examples) + (generate_project_file) (theories elpi elpi.json elpi.json.tests)) (include_subdirs qualified) diff --git a/apps/json/tests-plugin/dune b/apps/json/tests-plugin/dune index 0542035e6..d170ea9e9 100644 --- a/apps/json/tests-plugin/dune +++ b/apps/json/tests-plugin/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.json.tests) (package rocq-elpi-json-tests) + (generate_project_file) (theories elpi elpi.json)) ; work around missing dune support for Extra Dependency @@ -14,4 +15,4 @@ (progn (run rocq_elpi_shafile %{deps}))))) -(include_subdirs qualified) \ No newline at end of file +(include_subdirs qualified) diff --git a/apps/json/theories/dune b/apps/json/theories/dune index e5264dab3..3a13d3866 100644 --- a/apps/json/theories/dune +++ b/apps/json/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.json) (theories elpi_elpi elpi) + (generate_project_file) (plugins rocq-elpi-json.elpi_json_plugin) (package rocq-elpi-json)) diff --git a/apps/locker/elpi/dune b/apps/locker/elpi/dune index c2bdbf258..8d9a1256d 100644 --- a/apps/locker/elpi/dune +++ b/apps/locker/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.locker.elpi) (package rocq-elpi) + (generate_project_file) (theories elpi)) (rule diff --git a/apps/locker/tests/dune b/apps/locker/tests/dune index 4ca185a48..738b0ae8c 100644 --- a/apps/locker/tests/dune +++ b/apps/locker/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.locker.tests) (package rocq-elpi-tests) + (generate_project_file) (theories elpi elpi.apps.locker)) (include_subdirs qualified) diff --git a/apps/locker/theories/dune b/apps/locker/theories/dune index 0af01f2ae..51d30f451 100644 --- a/apps/locker/theories/dune +++ b/apps/locker/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.locker) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.locker.elpi)) (include_subdirs qualified) diff --git a/apps/rbuild/elpi/dune b/apps/rbuild/elpi/dune index af8ff66ec..ab539e7d7 100644 --- a/apps/rbuild/elpi/dune +++ b/apps/rbuild/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.rbuild.elpi) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.coercion)) (rule diff --git a/apps/rbuild/examples/dune b/apps/rbuild/examples/dune index e5610a4e6..33dde5086 100644 --- a/apps/rbuild/examples/dune +++ b/apps/rbuild/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.apps.rbuild.examples) + (generate_project_file) (theories elpi elpi.apps.rbuild elpi.apps.derive)) (include_subdirs qualified) diff --git a/apps/rbuild/theories/dune b/apps/rbuild/theories/dune index 7f8a16bd1..aaf71cc7c 100644 --- a/apps/rbuild/theories/dune +++ b/apps/rbuild/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.rbuild) (package rocq-elpi) + (generate_project_file) (theories elpi elpi.apps.rbuild.elpi elpi.apps.derive)) (include_subdirs qualified) diff --git a/apps/tc/elpi/dune b/apps/tc/elpi/dune index 8133f9d88..d272eb8cc 100644 --- a/apps/tc/elpi/dune +++ b/apps/tc/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.apps.tc.elpi) (package rocq-elpi) + (generate_project_file) (theories elpi)) (rule diff --git a/apps/tc/examples/dune b/apps/tc/examples/dune index 7deeb8084..e61dbd260 100644 --- a/apps/tc/examples/dune +++ b/apps/tc/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.apps.tc.examples) + (generate_project_file) (theories elpi elpi.apps.tc Stdlib)) (include_subdirs qualified) diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune index cc8497ee5..c5f240350 100644 --- a/apps/tc/tests-stdlib/dune +++ b/apps/tc/tests-stdlib/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi-tests-stdlib) (name elpi_apps_tc_tests_stdlib) + (package rocq-elpi-tests-stdlib) + (generate_project_file) (flags :standard -async-proofs-cache force) (theories elpi elpi.apps.tc elpi.apps.tc.tests Stdlib)) diff --git a/apps/tc/tests/dune b/apps/tc/tests/dune index 9f472d8f7..91a33f1e8 100644 --- a/apps/tc/tests/dune +++ b/apps/tc/tests/dune @@ -1,7 +1,8 @@ (rocq.theory (name elpi.apps.tc.tests) - (flags :standard -async-proofs-cache force) (package rocq-elpi-tests) + (generate_project_file) + (flags :standard -async-proofs-cache force) (theories elpi elpi.apps.tc)) (include_subdirs qualified) diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune index 2263bb9ea..fa99b17f4 100644 --- a/apps/tc/theories/dune +++ b/apps/tc/theories/dune @@ -1,8 +1,9 @@ (rocq.theory (name elpi.apps.tc) (package rocq-elpi) - (theories elpi elpi.apps.tc.elpi) + (generate_project_file) (flags -w -all -w -elpi) + (theories elpi elpi.apps.tc.elpi) (plugins rocq-elpi.tc)) (include_subdirs qualified) diff --git a/apps/xml/examples/dune b/apps/xml/examples/dune index 921cef7a3..35ae6a4f5 100644 --- a/apps/xml/examples/dune +++ b/apps/xml/examples/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.xml.examples) + (generate_project_file) (theories elpi elpi.xml elpi.xml.tests)) (include_subdirs qualified) diff --git a/apps/xml/tests-plugin/dune b/apps/xml/tests-plugin/dune index 95deeca57..97fdfc758 100644 --- a/apps/xml/tests-plugin/dune +++ b/apps/xml/tests-plugin/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi.xml.tests) (package rocq-elpi-xml-tests) + (generate_project_file) (theories elpi elpi.xml)) ; work around missing dune support for Extra Dependency @@ -14,4 +15,4 @@ (progn (run rocq_elpi_shafile %{deps}))))) -(include_subdirs qualified) \ No newline at end of file +(include_subdirs qualified) diff --git a/apps/xml/theories/dune b/apps/xml/theories/dune index c2560776f..5b394f555 100644 --- a/apps/xml/theories/dune +++ b/apps/xml/theories/dune @@ -1,7 +1,8 @@ (rocq.theory (name elpi.xml) - (theories elpi_elpi elpi) + (package rocq-elpi-xml) + (generate_project_file) (plugins rocq-elpi-xml.elpi_xml_plugin) - (package rocq-elpi-xml)) + (theories elpi_elpi elpi)) (include_subdirs qualified) diff --git a/elpi/dune b/elpi/dune index bf1b33f29..cbeb1c6fd 100644 --- a/elpi/dune +++ b/elpi/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi_elpi) ; FIXME - (package rocq-elpi)) + (package rocq-elpi) + (generate_project_file)) (rule (target dummy.v) diff --git a/examples-stdlib/dune b/examples-stdlib/dune index f0103f21f..e03340b1e 100644 --- a/examples-stdlib/dune +++ b/examples-stdlib/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi-tests-stdlib) (name elpi_examples_stdlib) + (package rocq-elpi-tests-stdlib) + (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi Stdlib)) diff --git a/examples/dune b/examples/dune index 62d3ddf7d..25a28f94e 100644 --- a/examples/dune +++ b/examples/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi) (name elpi_examples) + (package rocq-elpi) + (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi)) diff --git a/examples/example_plugin/elpi/dune b/examples/example_plugin/elpi/dune index 0dc0ba6c7..a7314ed0b 100644 --- a/examples/example_plugin/elpi/dune +++ b/examples/example_plugin/elpi/dune @@ -5,6 +5,7 @@ ; the rocq files in this folder (theories) ; will use the plugin defined in src (plugins myExtension.plugin) + (generate_project_file) (package myExtension)) (include_subdirs qualified) diff --git a/examples/example_plugin/tests/dune b/examples/example_plugin/tests/dune index 71af3e6dc..7f94bbab7 100644 --- a/examples/example_plugin/tests/dune +++ b/examples/example_plugin/tests/dune @@ -1,6 +1,7 @@ (rocq.theory (name myExtension.tests) (package myExtension-tests) + (generate_project_file) ; the tests folder depends on ext (theories elpi_elpi elpi myExtension myExtension.lib)) diff --git a/examples/example_plugin/theories/dune b/examples/example_plugin/theories/dune index 2d7cdee95..97b1b2b0c 100644 --- a/examples/example_plugin/theories/dune +++ b/examples/example_plugin/theories/dune @@ -8,6 +8,8 @@ ; will use the pluging called ext.plug ; the rocq files in this folder use the pluging defined in src/ (plugins myExtension.plugin) + ; indicate that a _RocqProject file should be generated + (generate_project_file) (package myExtension)) (include_subdirs qualified) diff --git a/tests-stdlib/dune b/tests-stdlib/dune index 5aec0e173..07edb6573 100644 --- a/tests-stdlib/dune +++ b/tests-stdlib/dune @@ -1,6 +1,7 @@ (rocq.theory - (package rocq-elpi-tests-stdlib) (name elpi_tests_stdlib) + (package rocq-elpi-tests-stdlib) + (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi Stdlib)) diff --git a/tests/dune b/tests/dune index 31c2a8b43..5f1fc24be 100644 --- a/tests/dune +++ b/tests/dune @@ -1,5 +1,6 @@ (rocq.theory (name elpi.tests) + (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi)) diff --git a/theories/dune b/theories/dune index 99d12482d..dcc4358e8 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,7 @@ (rocq.theory (name elpi) (package rocq-elpi) + (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi_elpi)) From 6f3120b09eccc3db59d0f73310d9d5a4ebd25b67 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 20 Aug 2026 14:48:20 +0200 Subject: [PATCH 3/3] Avoid dummy packages + generate opam files. --- apps/NES/tests/dune | 4 +-- apps/coercion/tests/dune | 4 +-- apps/derive/tests-stdlib/dune | 4 +-- apps/derive/tests/dune | 4 +-- apps/eltac/tests-stdlib/dune | 4 +-- apps/eltac/tests/dune | 4 +-- apps/json/tests-plugin/dune | 4 +-- apps/locker/tests/dune | 4 +-- apps/tc/tests-stdlib/dune | 1 - apps/tc/tests/dune | 1 - apps/xml/tests-plugin/dune | 4 +-- builtin-doc/coq-builtin.elpi | 3 +- builtin-doc/elpi-builtin.elpi | 9 ++---- dune-project | 40 ++++++------------------ etc/with-rocq-wrap.sh | 59 ----------------------------------- examples-stdlib/dune | 4 +-- rocq-elpi-json.opam | 9 +++--- rocq-elpi-xml.opam | 9 +++--- rocq-elpi.opam | 5 ++- tests-stdlib/dune | 4 +-- 20 files changed, 38 insertions(+), 142 deletions(-) delete mode 100755 etc/with-rocq-wrap.sh diff --git a/apps/NES/tests/dune b/apps/NES/tests/dune index 7f68cbe3d..4d8532593 100644 --- a/apps/NES/tests/dune +++ b/apps/NES/tests/dune @@ -1,8 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi.apps.NES.tests) - (package rocq-elpi-tests) (generate_project_file) (theories elpi elpi.apps.NES)) -(include_subdirs qualified) - diff --git a/apps/coercion/tests/dune b/apps/coercion/tests/dune index 8b467b767..638266887 100644 --- a/apps/coercion/tests/dune +++ b/apps/coercion/tests/dune @@ -1,7 +1,5 @@ +(include_subdirs qualified) (rocq.theory (name elpi.apps.coercion.tests) - (package rocq-elpi-tests) (generate_project_file) (theories elpi elpi.apps.coercion)) - -(include_subdirs qualified) diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune index 141ca6410..757b48ec0 100644 --- a/apps/derive/tests-stdlib/dune +++ b/apps/derive/tests-stdlib/dune @@ -1,8 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi_apps_derive_tests_stdlib) - (package rocq-elpi-tests-stdlib) (generate_project_file) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive elpi.apps.derive.tests Stdlib)) - -(include_subdirs qualified) diff --git a/apps/derive/tests/dune b/apps/derive/tests/dune index 678b202c9..9d68f3a65 100644 --- a/apps/derive/tests/dune +++ b/apps/derive/tests/dune @@ -1,8 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi.apps.derive.tests) - (package rocq-elpi-tests) (generate_project_file) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive)) - -(include_subdirs qualified) diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune index 6b9679168..def08a906 100644 --- a/apps/eltac/tests-stdlib/dune +++ b/apps/eltac/tests-stdlib/dune @@ -1,7 +1,5 @@ +(include_subdirs qualified) (rocq.theory (name elpi_apps_eltac_tests_stdlib) - (package rocq-elpi-tests-stdlib) (generate_project_file) (theories elpi elpi.apps.eltac Stdlib)) - -(include_subdirs qualified) diff --git a/apps/eltac/tests/dune b/apps/eltac/tests/dune index c632ef75d..2c45d7e8f 100644 --- a/apps/eltac/tests/dune +++ b/apps/eltac/tests/dune @@ -1,7 +1,5 @@ +(include_subdirs qualified) (rocq.theory (name elpi.apps.eltac.tests) - (package rocq-elpi-tests) (generate_project_file) (theories elpi elpi.apps.eltac)) - -(include_subdirs qualified) diff --git a/apps/json/tests-plugin/dune b/apps/json/tests-plugin/dune index d170ea9e9..f2a0a7f08 100644 --- a/apps/json/tests-plugin/dune +++ b/apps/json/tests-plugin/dune @@ -1,6 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi.json.tests) - (package rocq-elpi-json-tests) (generate_project_file) (theories elpi elpi.json)) @@ -14,5 +14,3 @@ (with-stdout-to %{target} (progn (run rocq_elpi_shafile %{deps}))))) - -(include_subdirs qualified) diff --git a/apps/locker/tests/dune b/apps/locker/tests/dune index 738b0ae8c..86daecb4c 100644 --- a/apps/locker/tests/dune +++ b/apps/locker/tests/dune @@ -1,7 +1,5 @@ +(include_subdirs qualified) (rocq.theory (name elpi.apps.locker.tests) - (package rocq-elpi-tests) (generate_project_file) (theories elpi elpi.apps.locker)) - -(include_subdirs qualified) diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune index c5f240350..568f9ae14 100644 --- a/apps/tc/tests-stdlib/dune +++ b/apps/tc/tests-stdlib/dune @@ -1,6 +1,5 @@ (rocq.theory (name elpi_apps_tc_tests_stdlib) - (package rocq-elpi-tests-stdlib) (generate_project_file) (flags :standard -async-proofs-cache force) (theories elpi elpi.apps.tc elpi.apps.tc.tests Stdlib)) diff --git a/apps/tc/tests/dune b/apps/tc/tests/dune index 91a33f1e8..7c31e28c2 100644 --- a/apps/tc/tests/dune +++ b/apps/tc/tests/dune @@ -1,6 +1,5 @@ (rocq.theory (name elpi.apps.tc.tests) - (package rocq-elpi-tests) (generate_project_file) (flags :standard -async-proofs-cache force) (theories elpi elpi.apps.tc)) diff --git a/apps/xml/tests-plugin/dune b/apps/xml/tests-plugin/dune index 97fdfc758..9d19ad8e3 100644 --- a/apps/xml/tests-plugin/dune +++ b/apps/xml/tests-plugin/dune @@ -1,6 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi.xml.tests) - (package rocq-elpi-xml-tests) (generate_project_file) (theories elpi elpi.xml)) @@ -14,5 +14,3 @@ (with-stdout-to %{target} (progn (run rocq_elpi_shafile %{deps}))))) - -(include_subdirs qualified) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 6252b244e..90f8c890e 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -1518,7 +1518,8 @@ external func coq.typecheck term -> term, diagnostic. external func coq.typecheck-ty term -> sort, diagnostic. % [coq.typecheck-relevance T T1] recomputes by retyping the relevance -% mark of every binder of T: binders whose type lives in SProp become +% mark of every binder of T: binders whose type lives in SProp +% become % irrelevant, the others relevant. A binder whose type does not retype % keeps the mark it has. The kernel checks these marks, so a term % assembled by hand rather than obtained from elaboration may need this. diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi index 35aece17f..7127be336 100644 --- a/builtin-doc/elpi-builtin.elpi +++ b/builtin-doc/elpi-builtin.elpi @@ -532,14 +532,11 @@ length [_|L] N :- length L N1, N is N1 + 1. length [] 0. func rev list A -> list A. -rev L RL :- rev-append L [] RL. - -func rev-append list A, list A -> list A. -rev-append [X|XS] ACC R :- rev-append XS [X|ACC] R. -rev-append [] L L. +rev L RL :- rev.aux L [] RL. func rev.aux list A, list A -> list A. -rev.aux L1 L2 L3 :- rev-append L1 L2 L3. +rev.aux [X|XS] ACC R :- rev.aux XS [X|ACC] R. +rev.aux [] L L. func last list A -> A. last [] _ :- fatal-error "last on empty list". diff --git a/dune-project b/dune-project index 4a9c0e82b..85be2e356 100644 --- a/dune-project +++ b/dune-project @@ -1,7 +1,7 @@ (lang dune 3.21) (using rocq 0.11) (name rocq-elpi) -;(generate_opam_files) +(generate_opam_files) (source (github LPCIC/coq-elpi)) (license LGPL-2.1-or-later) @@ -30,43 +30,23 @@ "logpath:elpi")) (depends (ocaml (>= 4.10.0)) - (elpi (and (>= 3.0) (< 3.2.0~))) - ; (rocq-core (and (>= 9.0+rc1) (< 9.2~))) + (elpi (and (>= 3.7.1) (< 3.8.0~))) + (rocq-core (or (and (>= 9.0+rc1) (< 9.4~)) (= dev))) ppx_optcomp (ocaml-lsp-server :with-dev-setup))) (package (name rocq-elpi-json) (synopsis "Yojson bindings for rocq-elpi") - (description "This package provides basic support for reading and writing json files from Elpi programs running in Rocq") + (description + "This package provides basic support for reading and writing json files \ + from Elpi programs running in Rocq") (depends rocq-elpi yojson)) (package (name rocq-elpi-xml) (synopsis "Xml-light bindings for rocq-elpi") - (description "DThis package provides basic support for reading xml files from Elpi programs running in Rocq") - (depends rocq-elpi yojson)) - -(package - (name rocq-elpi-tests) - (synopsis "Technical package to run tests") - (description "Do not install") - (depends rocq-elpi)) - -(package - (name rocq-elpi-json-tests) - (synopsis "Technical package to run tests") - (description "Do not install") - (depends rocq-elpi)) - -(package - (name rocq-elpi-xml-tests) - (synopsis "Technical package to run tests") - (description "Do not install") - (depends rocq-elpi)) - -(package - (name rocq-elpi-tests-stdlib) - (synopsis "Technical package to run tests depending on Stdlib") - (description "Do not install") - (depends rocq-elpi rocq-stdlib)) + (description + "This package provides basic support for reading xml files from Elpi \ + programs running in Rocq") + (depends rocq-elpi xml-light)) diff --git a/etc/with-rocq-wrap.sh b/etc/with-rocq-wrap.sh deleted file mode 100755 index 0dd7db9da..000000000 --- a/etc/with-rocq-wrap.sh +++ /dev/null @@ -1,59 +0,0 @@ -#!/usr/bin/env bash - -set -ex - -rocq=$(command -v rocq) -# NB on cygwin "$rocq" is a cygwin path (/foo/bar) -# but reading files from hash.exe needs windows paths (C:/cygwin/foo/bar) -# we avoid the problem by going through stdin -rocqhash=$(dune exec --root "$(dirname "$0")"/.. -- etc/tools/hash.exe < "$rocq") - -rm -rf .wrappers -mkdir .wrappers - -cat > .wrappers/coqc < .wrappers/coqdep < .wrappers/coqdoc < .wrappers/coqpp < .wrappers/META.coq-core <"] authors: ["Enrico Tassi "] license: "LGPL-2.1-or-later" -homepage: "https://github.com/LPCIC/coq-elpi/apps/json/" +homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.21"} "rocq-elpi" "yojson" "odoc" {with-doc} @@ -16,7 +17,6 @@ depends: [ build: [ ["dune" "subst"] {dev} [ - "etc/with-rocq-wrap.sh" {!coq-core:installed} "dune" "build" "-p" @@ -29,3 +29,4 @@ build: [ ] ] dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" +x-maintenance-intent: ["(latest)"] diff --git a/rocq-elpi-xml.opam b/rocq-elpi-xml.opam index 48bac3080..34617e8cb 100644 --- a/rocq-elpi-xml.opam +++ b/rocq-elpi-xml.opam @@ -1,14 +1,15 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" synopsis: "Xml-light bindings for rocq-elpi" -description: "This package provides basic support for reading xml files from Elpi programs running in Rocq" +description: + "This package provides basic support for reading xml files from Elpi programs running in Rocq" maintainer: ["Enrico Tassi "] authors: ["Enrico Tassi "] license: "LGPL-2.1-or-later" -homepage: "https://github.com/LPCIC/coq-elpi/apps/xml/" +homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.21"} "rocq-elpi" "xml-light" "odoc" {with-doc} @@ -16,7 +17,6 @@ depends: [ build: [ ["dune" "subst"] {dev} [ - "etc/with-rocq-wrap.sh" {!coq-core:installed} "dune" "build" "-p" @@ -29,3 +29,4 @@ build: [ ] ] dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" +x-maintenance-intent: ["(latest)"] diff --git a/rocq-elpi.opam b/rocq-elpi.opam index 65ebb0832..e48f65148 100644 --- a/rocq-elpi.opam +++ b/rocq-elpi.opam @@ -15,19 +15,17 @@ tags: [ homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} + "dune" {>= "3.21"} "ocaml" {>= "4.10.0"} "elpi" {>= "3.7.1" & < "3.8.0~"} "rocq-core" {>= "9.0+rc1" & < "9.4~" | = "dev"} "ppx_optcomp" "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc} - "rocq-stdlib" {with-doc} ] build: [ ["dune" "subst"] {dev} [ - "etc/with-rocq-wrap.sh" {!coq-core:installed} "dune" "build" "-p" @@ -40,3 +38,4 @@ build: [ ] ] dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" +x-maintenance-intent: ["(latest)"] diff --git a/tests-stdlib/dune b/tests-stdlib/dune index 07edb6573..37aa56ea6 100644 --- a/tests-stdlib/dune +++ b/tests-stdlib/dune @@ -1,8 +1,6 @@ +(include_subdirs qualified) (rocq.theory (name elpi_tests_stdlib) - (package rocq-elpi-tests-stdlib) (generate_project_file) (plugins rocq-elpi.elpi) (theories elpi Stdlib)) - -; (include_subdirs qualified)