From 5e0c4ced5fa84f0e0b9ad4c6cc42f49d789c833c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 9 Jun 2026 10:53:10 +0200 Subject: [PATCH 1/7] add builtin to add one class to the list of classes solved by elpi's tc solver --- apps/tc/doc/dune | 16 ++++++++++ apps/tc/doc/gen_doc.ml | 3 ++ .../src/rocq_elpi_class_tactics_takeover.ml | 10 +++++++ .../src/rocq_elpi_class_tactics_takeover.mli | 1 + dune-project | 6 ++++ rocq-elpi-tc.opam | 29 +++++++++++++++++++ 6 files changed, 65 insertions(+) create mode 100644 apps/tc/doc/dune create mode 100644 apps/tc/doc/gen_doc.ml create mode 100644 rocq-elpi-tc.opam diff --git a/apps/tc/doc/dune b/apps/tc/doc/dune new file mode 100644 index 000000000..ca4635ea5 --- /dev/null +++ b/apps/tc/doc/dune @@ -0,0 +1,16 @@ +(executable + (name gen_doc) + (libraries elpi_tc_plugin)) + +(rule + (targets + tc-builtin.elpi) + (deps gen_doc.exe) + (mode promote) + (action (run ./gen_doc.exe))) + +(install + (files + tc-builtin.elpi) + (section doc) + (package rocq-elpi-tc)) diff --git a/apps/tc/doc/gen_doc.ml b/apps/tc/doc/gen_doc.ml new file mode 100644 index 000000000..3130a43b4 --- /dev/null +++ b/apps/tc/doc/gen_doc.ml @@ -0,0 +1,3 @@ + +let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated" + Elpi_tc_plugin.Rocq_elpi_class_tactics_takeover.tc_builtins diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml index 7a2c98085..24011d4e1 100644 --- a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml @@ -180,6 +180,16 @@ let set_solver_mode kind qname (l: Libnames.qualid list) = | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false)) | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only l), false)) +let tc_builtins = [ + Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", + In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", + Easy("Declares that goals on GR should be solved using elpi's typeclass solver.")), + (fun gr ~depth -> + set_solver_mode AAdd ["TC.Solver"] (List.map Libnames.qualid_of_string gr))), + DocAbove)] + +let tc_builtins = API.BuiltIn.declare ~file_name:"tc-builtin.elpi" tc_builtins + let solver_register l = Lib.add_leaf (Solver.cache_solver (l, Create)); Lib.add_leaf (Modes.cache_solver_mode (l, Add OSet.empty, true)) diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.mli b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli index 49ecce52c..062bf26e8 100644 --- a/apps/tc/src/rocq_elpi_class_tactics_takeover.mli +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli @@ -8,3 +8,4 @@ val set_solver_mode : aaction -> string list -> Libnames.qualid list -> unit val solver_register : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit val solver_activate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit val solver_deactivate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit +val tc_builtins : Elpi.API.Setup.builtins diff --git a/dune-project b/dune-project index a71a5bd67..82f27b3e6 100644 --- a/dune-project +++ b/dune-project @@ -35,6 +35,12 @@ ppx_optcomp (ocaml-lsp-server :with-dev-setup))) +(package + (name rocq-elpi-tc) + (synopsis "TC bindings for rocq-elpi") + (description "This package provides a typeclass solver written in Elpi for Rocq") + (depends rocq-elpi)) + (package (name rocq-elpi-json) (synopsis "Yojson bindings for rocq-elpi") diff --git a/rocq-elpi-tc.opam b/rocq-elpi-tc.opam new file mode 100644 index 000000000..98ce6df3e --- /dev/null +++ b/rocq-elpi-tc.opam @@ -0,0 +1,29 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "TC bindings for rocq-elpi" +description: "This package provides a typeclass solver written in Elpi for Rocq" +maintainer: ["Enrico Tassi "] +authors: ["Enrico Tassi "] +license: "LGPL-2.1-or-later" +homepage: "https://github.com/LPCIC/coq-elpi/apps/tc/" +bug-reports: "https://github.com/LPCIC/coq-elpi/issues" +depends: [ + "dune" {>= "3.13"} + "rocq-elpi" +] +build: [ + ["dune" "subst"] {dev} + [ + "etc/with-rocq-wrap.sh" {!coq-core:installed} + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" From 60b1839088afb36d8a3e7abc78c1c9fd99553cd8 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 9 Jun 2026 12:33:04 +0200 Subject: [PATCH 2/7] rename package and fix name in src/dune --- apps/tc/doc/dune | 2 +- apps/tc/src/dune | 2 +- dune-project | 2 +- rocq-elpi-tc.opam => rocq-elpi-typeclasses.opam | 0 4 files changed, 3 insertions(+), 3 deletions(-) rename rocq-elpi-tc.opam => rocq-elpi-typeclasses.opam (100%) diff --git a/apps/tc/doc/dune b/apps/tc/doc/dune index ca4635ea5..5efc1871f 100644 --- a/apps/tc/doc/dune +++ b/apps/tc/doc/dune @@ -13,4 +13,4 @@ (files tc-builtin.elpi) (section doc) - (package rocq-elpi-tc)) + (package rocq-elpi-typeclasses)) diff --git a/apps/tc/src/dune b/apps/tc/src/dune index 6c60a9c10..ebc96e820 100644 --- a/apps/tc/src/dune +++ b/apps/tc/src/dune @@ -1,6 +1,6 @@ (library (name elpi_tc_plugin) - (public_name rocq-elpi.tc) + (public_name rocq-elpi-typeclasses.elpi_tc_plugin) (flags :standard -w -27) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi)) diff --git a/dune-project b/dune-project index 82f27b3e6..550185405 100644 --- a/dune-project +++ b/dune-project @@ -36,7 +36,7 @@ (ocaml-lsp-server :with-dev-setup))) (package - (name rocq-elpi-tc) + (name rocq-elpi-typeclasses) (synopsis "TC bindings for rocq-elpi") (description "This package provides a typeclass solver written in Elpi for Rocq") (depends rocq-elpi)) diff --git a/rocq-elpi-tc.opam b/rocq-elpi-typeclasses.opam similarity index 100% rename from rocq-elpi-tc.opam rename to rocq-elpi-typeclasses.opam From b3dfd612abdd59f946f4320300ce4e378ca9f805 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 9 Jun 2026 12:45:30 +0200 Subject: [PATCH 3/7] fix theories/dune --- apps/tc/theories/dune | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune index 6e7a83821..3164f3262 100644 --- a/apps/tc/theories/dune +++ b/apps/tc/theories/dune @@ -1,8 +1,8 @@ (coq.theory (name elpi.apps.tc) - (package rocq-elpi) + (package rocq-elpi-typeclasses) (theories elpi elpi.apps.tc.elpi) (flags -w -all -w -elpi) - (plugins rocq-elpi.tc)) + (plugins rocq-elpi-typeclasses.elpi_tc_plugin)) (include_subdirs qualified) From a1cbff79ce85d7e9ce75d5a0235393ab78feaa2d Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 12 Jun 2026 15:21:23 +0200 Subject: [PATCH 4/7] fix plugin name in .v files --- apps/tc/src/rocq_elpi_tc_hook.mlg | 4 ++-- apps/tc/theories/tc.v | 2 +- apps/tc/theories/wip.v | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/apps/tc/src/rocq_elpi_tc_hook.mlg b/apps/tc/src/rocq_elpi_tc_hook.mlg index 8c84d8855..9170c30fd 100644 --- a/apps/tc/src/rocq_elpi_tc_hook.mlg +++ b/apps/tc/src/rocq_elpi_tc_hook.mlg @@ -1,7 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -DECLARE PLUGIN "rocq-elpi.tc" +DECLARE PLUGIN "rocq-elpi-typeclasses.elpi_tc_plugin" { open Stdarg @@ -51,4 +51,4 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF let () = ignore_unknown_attributes atts in set_solver_mode ARm (snd p) cs } -END \ No newline at end of file +END diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 31cc2d4b9..98c7bb906 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -1,7 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -Declare ML Module "rocq-elpi.tc". +Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin". From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux. (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *) diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v index d7060d727..5e45f5a96 100644 --- a/apps/tc/theories/wip.v +++ b/apps/tc/theories/wip.v @@ -1,7 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* --------------------------------------------------------------------------*) -Declare ML Module "rocq-elpi.tc". +Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin". From elpi Require Import elpi. From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes. From dc9956fee1cf321fb0140f9a8ce0cd7a74949f6b Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 12 Jun 2026 16:45:36 +0200 Subject: [PATCH 5/7] fix dune files --- apps/tc/theories/dune | 4 ++-- apps/tc/theories/tc.v | 1 + apps/tc/theories/wip.v | 5 +++-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune index 3164f3262..bcfd269b4 100644 --- a/apps/tc/theories/dune +++ b/apps/tc/theories/dune @@ -1,8 +1,8 @@ (coq.theory (name elpi.apps.tc) (package rocq-elpi-typeclasses) - (theories elpi elpi.apps.tc.elpi) + (theories elpi_elpi elpi elpi.apps.tc.elpi) (flags -w -all -w -elpi) - (plugins rocq-elpi-typeclasses.elpi_tc_plugin)) + (plugins rocq-elpi.elpi rocq-elpi-typeclasses.elpi_tc_plugin)) (include_subdirs qualified) diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 98c7bb906..510f2bd34 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -1,6 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) +From elpi Require Import elpi. Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin". From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux. diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v index 5e45f5a96..f526c99fd 100644 --- a/apps/tc/theories/wip.v +++ b/apps/tc/theories/wip.v @@ -1,8 +1,9 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* --------------------------------------------------------------------------*) -Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin". +(* From elpi Require Import elpi. +Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin". From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes. From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile. @@ -16,7 +17,7 @@ From elpi.apps.tc.elpi Extra Dependency "rewrite_forward.elpi" as rforward. From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux. From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate. -(* From elpi.apps Require Import tc. +From elpi.apps Require Import tc. Set Warnings "+elpi". Elpi Command AddForwardRewriting. From 2933a3a177e3ee46b0a397e8b3cbe80a1634354d Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 17 Jun 2026 15:29:09 +0200 Subject: [PATCH 6/7] review --- .github/workflows/release.yml | 2 +- Changelog.md | 6 ++++++ apps/tc/src/rocq_elpi_class_tactics_takeover.ml | 7 ++++--- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 3ab119660..ff2dd5fa7 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -98,6 +98,6 @@ jobs: GITHUB_DEBUG=1 opam-publish --no-confirmation --tag=$TAG \ --packages-directory=${OPAM_SUITE:-released}/packages \ --repo=rocq-prover/opam --no-browser -v ${TAG##v} \ - rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam \ + rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam rocq-elpi-typeclasses.opam\ coq-elpi.opam \ https://github.com/LPCIC/coq-elpi/releases/download/$TAG/rocq-elpi-${TAG##v}.tar.gz diff --git a/Changelog.md b/Changelog.md index 684e4f4ad..0808dda62 100644 --- a/Changelog.md +++ b/Changelog.md @@ -21,6 +21,12 @@ Requires Elpi 3.7.1 and Rocq 9.0, 9.1 or 9.2. ### Plugins - New `xml` plugin containing minimal bindings to `xml-light`, see [apps/xml](apps/xml/) for the doc. +- New `typeclasses` plugin containing rocq-elpi's typeclass solver, see + [apps/tc](apps/tc/) for the doc. + +### API +- New `coq.TC.override-solver` builtin calling the + `Elpi TC Solver Override _ Add _` directive. ### API - Change `main-interp-proof` and `main-interp-qed` changed type to better chain diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml index 24011d4e1..0009a2a6b 100644 --- a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml @@ -182,10 +182,11 @@ let set_solver_mode kind qname (l: Libnames.qualid list) = let tc_builtins = [ Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", + In(Elpi.API.BuiltInData.string, "GR", In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", - Easy("Declares that goals on GR should be solved using elpi's typeclass solver.")), - (fun gr ~depth -> - set_solver_mode AAdd ["TC.Solver"] (List.map Libnames.qualid_of_string gr))), + Easy("Declares that goals on GR should be solved using elpi's typeclass solver."))), + (fun s gr ~depth -> + set_solver_mode AAdd [s] (List.map Libnames.qualid_of_string gr))), DocAbove)] let tc_builtins = API.BuiltIn.declare ~file_name:"tc-builtin.elpi" tc_builtins From 2e52cf4ee4bddb5be001b4d2326469fc666604fd Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 17 Jun 2026 17:20:54 +0200 Subject: [PATCH 7/7] review --- apps/tc/src/rocq_elpi_class_tactics_takeover.ml | 6 +++--- dune-project | 4 ++-- rocq-elpi-typeclasses.opam | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml index 0009a2a6b..2cea25d0b 100644 --- a/apps/tc/src/rocq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml @@ -182,9 +182,9 @@ let set_solver_mode kind qname (l: Libnames.qualid list) = let tc_builtins = [ Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver", - In(Elpi.API.BuiltInData.string, "GR", - In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR", - Easy("Declares that goals on GR should be solved using elpi's typeclass solver."))), + In(Elpi.API.BuiltInData.string, "SolverName", + In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "ClassNames", + Easy("Declares that goals on classes in ClassNames should be solved using the typeclass solver SolverName."))), (fun s gr ~depth -> set_solver_mode AAdd [s] (List.map Libnames.qualid_of_string gr))), DocAbove)] diff --git a/dune-project b/dune-project index 550185405..e61b7179d 100644 --- a/dune-project +++ b/dune-project @@ -37,8 +37,8 @@ (package (name rocq-elpi-typeclasses) - (synopsis "TC bindings for rocq-elpi") - (description "This package provides a typeclass solver written in Elpi for Rocq") + (synopsis "Typeclass solver in rocq-elpi") + (description "This package provides a typeclass solver written in Elpi, as well as the infrastructure for writing custom ones") (depends rocq-elpi)) (package diff --git a/rocq-elpi-typeclasses.opam b/rocq-elpi-typeclasses.opam index 98ce6df3e..61a6f9515 100644 --- a/rocq-elpi-typeclasses.opam +++ b/rocq-elpi-typeclasses.opam @@ -1,7 +1,7 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" synopsis: "TC bindings for rocq-elpi" -description: "This package provides a typeclass solver written in Elpi for Rocq" +description: "This package provides a typeclass solver written in Elpi, as well as the infrastructure for writing custom ones" maintainer: ["Enrico Tassi "] authors: ["Enrico Tassi "] license: "LGPL-2.1-or-later"