Typeclass-based Ltac2 dispatch. by gmalecha-at-skylabs · Pull Request #96 · SkyLabsAI/BRiCk

gmalecha-at-skylabs · 2026-03-26T16:44:09Z

A sketch proposal for resolving an Ltac2 function using typeclasses.

rocq-ltac2-tc-dispatch/plugin/lookup.ml

rocq-ltac2-tc-dispatch/README.md

skylabs-ai-ci · 2026-03-26T16:55:57Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	gmalecha/tc-based-ltac2-dispatch	e59ba9e	main	6464439	#96

Passive Repos

Repo	Job Branch	Job Commit
./	main	1a623c6
fmdeps/auto/	main	2193cc6
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	2ccdf85
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.00%	123316.4	123317.6	+1.2	total
+0.00%	-	1.2	+1.2	├ newly appeared files (1)
-0.00%	123316.4	123316.4	-0.0	└ common files
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.00%	100689.8	100689.8	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	123316.4	123317.6	+1.2	total
+0.00%	-	1.2	+1.2	├ newly appeared files (1)
-0.00%	123316.4	123316.4	-0.0	└ common files
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.00%	100689.8	100689.8	+0.0	└ proofs and tests

rocq-ltac2-tc-dispatch/README.md

skylabs-ai-ci · 2026-03-27T20:00:44Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	gmalecha/tc-based-ltac2-dispatch	286433a	main	238d10c	#96

Passive Repos

Repo	Job Branch	Job Commit
./	main	655dc44
fmdeps/auto/	main	215fe77
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	6060926
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.00%	123284.5	123290.6	+6.1	total
+0.00%	-	6.1	+6.1	├ newly appeared files (5)
+0.00%	123284.5	123284.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100657.9	100657.9	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	123284.5	123290.6	+6.1	total
+0.00%	-	6.1	+6.1	├ newly appeared files (5)
+0.00%	123284.5	123284.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100657.9	100657.9	+0.0	└ proofs and tests

rocq-ltac2-tc-dispatch/theories/lookup.v

SkySkimmer · 2026-03-28T13:01:23Z

rocq-ltac2-tc-dispatch/plugin/lookup.ml

+let resolve_ltac2_safe (mp : string list) (id : string) : (unit -> unit Proofview.tactic) option =
+  let qualid = Libnames.make_qualid
+    (Names.DirPath.make (List.map Names.Id.of_string mp))
+    (Names.Id.of_string id)


Why not take a single string (containing .) and call qualid_of_string on it instead of taking string list + string and calling make_qualid?
That way conversion is simpler (no list_of_list_constr) and you don't have to remember which order the list needs to be in.

This makes sense. Alternatively, I was thinking that we could get the module path from the constant of the type class instance. That makes it less fragile to move things around.

SkySkimmer · 2026-03-28T13:03:56Z

rocq-ltac2-tc-dispatch/plugin/lookup.ml

+    (Names.Id.of_string id)
+  in
+  let is_unit_typ (t : int Tac2expr.glb_typexpr) : bool =
+    (* TODO: why does Init.unit have two different representations? *)


because you don't normalize it (cf what Tac2typing_env.kind does)

SkySkimmer · 2026-03-28T13:08:34Z

rocq-ltac2-tc-dispatch/plugin/lookup.ml

+    | Tac2expr.GTypArrow (t1, t2) -> is_unit_typ t1 && is_unit_typ t2
+    | _ -> false
+  in
+  match Tac2env.locate_ltac qualid with


I guess we don't expose the full_path based API but if we did would you want to use it?
The difference with locate is that locate will resolve short names, so for instance locate on case will succeed when Control is imported but the full path based API would need Ltac2.Control.case regardless of importing.

For this use case, I would want to use definite references. Resolution at this level seems very awkward.

rocq-ltac2-tc-dispatch/plugin/lookup.ml

SkySkimmer · 2026-03-28T13:11:36Z

rocq-ltac2-tc-dispatch/plugin/lookup.ml

+    then
+      let v = Tac2interp.eval_global kn in
+      Some (repr_to (fun1 unit unit) v)
+    else None


might want to return a result with some error message to distinguish between "could not resolve" "resolved to non constant (Abbreviation)" and "resolved to constant of incorrect type"

I think this is a good idea, but I need to dig a bit more into the plugin API to figure out how to raise exceptions and such.

I said return result not raise though?

I actually need to figure out how to do that as well. This API is pretty foreign to me.

rocq-ltac2-tc-dispatch/theories/lookup.v

skylabs-ai-ci · 2026-03-29T01:32:45Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	gmalecha/tc-based-ltac2-dispatch	2eea27d	main	238d10c	#96

Passive Repos

Repo	Job Branch	Job Commit
./	main	655dc44
fmdeps/auto/	main	fbd79d5
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	6060926
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.00%	123290.5	123296.6	+6.1	total
+0.00%	-	6.1	+6.1	├ newly appeared files (5)
+0.00%	123290.5	123290.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	123290.5	123296.6	+6.1	total
+0.00%	-	6.1	+6.1	├ newly appeared files (5)
+0.00%	123290.5	123290.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

skylabs-ai-ci · 2026-03-29T02:04:22Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	gmalecha/tc-based-ltac2-dispatch	7878874	main	238d10c	#96

Passive Repos

Repo	Job Branch	Job Commit
./	main	655dc44
fmdeps/auto/	main	fbd79d5
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	6060926
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.01%	123290.5	123297.8	+7.3	total
+0.01%	-	7.3	+7.3	├ newly appeared files (6)
+0.00%	123290.5	123290.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.01%	123290.5	123297.8	+7.3	total
+0.01%	-	7.3	+7.3	├ newly appeared files (6)
+0.00%	123290.5	123290.5	+0.0	└ common files
+0.00%	22626.6	22626.6	+0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

skylabs-ai-ci · 2026-03-29T18:43:37Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/BRiCk/	gmalecha/tc-based-ltac2-dispatch	19f3f34	main	238d10c	#96

Passive Repos

Repo	Job Branch	Job Commit
./	main	655dc44
fmdeps/auto/	main	fbd79d5
fmdeps/auto-docs/	main	9f57097
bluerock/NOVA/	skylabs-proof	996d600
bluerock/bhv/	skylabs-main	8030a8f
fmdeps/brick-libcpp/	main	d30c178
fmdeps/ci/	main	9ecdef9
vendored/elpi/	skylabs-master	aa4475f
fmdeps/fm-ci/	main	262fb04
fmdeps/fm-tools/	main	e17f6db
psi/protos/	main	8fe3e7c
psi/backend/	main	99def76
psi/ide/	main	6b596cf
psi/data/	main	1c11c15
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	6060926
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
fmdeps/skylabs-fm/	main	7c3aae7
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+0.01%	123290.5	123297.8	+7.3	total
+0.01%	-	7.3	+7.3	├ newly appeared files (6)
-0.00%	123290.5	123290.5	-0.0	└ common files
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.01%	123290.5	123297.8	+7.3	total
+0.01%	-	7.3	+7.3	├ newly appeared files (6)
-0.00%	123290.5	123290.5	-0.0	└ common files
-0.00%	22626.6	22626.6	-0.0	├ translation units
+0.00%	100663.9	100663.9	+0.0	└ proofs and tests

rlepigre-skylabs-ai · 2026-03-30T08:03:02Z

rocq-ltac2-tc-dispatch/dune-project

+(authors
+ "Gregory Malecha <gregory@skylabs-ai.com>")
+
+(license MIT)


Why is there a LICENSE-LGPL file then?

We should change to LGPL to encourage contributions over forking.

rlepigre-skylabs-ai · 2026-03-30T08:04:04Z

rocq-ltac2-tc-dispatch/plugin/dune

+(library
+ (name ltac2_tc_dispatch)
+ (public_name ltac2-tc-dispatch.plugin)
+ (libraries coq-core.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))


Suggested change

(libraries coq-core.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))

(libraries rocq-runtime.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))

rlepigre-skylabs-ai · 2026-03-30T08:26:55Z

rocq-ltac2-tc-dispatch/theories/lookup.v

+(* The typeclass: P is the goal/type, path is the module hierarchy, name is the tactic *)
+Class Ltac2Lookup (P : Prop) := {
+    ltac2_path : list string;
+    ltac2_name : string;
+  }.


I guess we could add a new vernacular command for populating this class, and also checking the type of the given Ltac2 value.

Janno · 2026-03-30T09:18:51Z

I wonder if we should use dummy Rocq definitions to get the module paths automatically right. The simplest way would be to demand a definition of the same name as the tactic. That definition is used in the instance. No strings. At registration time, we check that a tactic of the same name exists. (And that it is not private.. we should check that anyway.)

This should allow us to not mention any module paths and Rocq will make sure that everything keeps working across module boundaries.

We could do the check in tactic-in-terms (or TC search) in the class constructor if we wanted to avoid a new vernacular command.

gmalecha-at-skylabs · 2026-03-30T11:02:17Z

@Janno I mentioned a similar idea on the Rocq Zulip. I'm not completely certain how to implement this, but all the data should be there.

On a related note, I was thinking that we might be able to support:

Calling regular Ltac tactics
Passing arguments to tactics from the arguments of the typeclass, e.g. a constr for each argument.

Both seem optional, but could be useful.

gmalecha-at-skylabs self-assigned this Mar 26, 2026

gmalecha-at-skylabs requested a review from Janno March 26, 2026 16:44

gmalecha-at-skylabs commented Mar 26, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/plugin/lookup.ml Outdated Show resolved Hide resolved

gmalecha-at-skylabs commented Mar 26, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/README.md Outdated Show resolved Hide resolved

gmalecha-at-skylabs commented Mar 27, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/README.md Outdated Show resolved Hide resolved

gmalecha-at-skylabs force-pushed the gmalecha/tc-based-ltac2-dispatch branch from d474fab to 4455298 Compare March 27, 2026 19:47

SkySkimmer reviewed Mar 28, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/theories/lookup.v Outdated Show resolved Hide resolved

SkySkimmer reviewed Mar 28, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/plugin/lookup.ml Outdated Show resolved Hide resolved

SkySkimmer reviewed Mar 28, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/plugin/lookup.ml Outdated Show resolved Hide resolved

SkySkimmer reviewed Mar 28, 2026

View reviewed changes

rocq-ltac2-tc-dispatch/theories/lookup.v Outdated Show resolved Hide resolved

Typeclass-based Ltac2 dispatch.

f1c41f8

gmalecha-at-skylabs force-pushed the gmalecha/tc-based-ltac2-dispatch branch from dffa510 to f1c41f8 Compare March 29, 2026 01:24

Sketch of an extensible implementation of crush.

e721ac7

gmalecha-at-skylabs force-pushed the gmalecha/tc-based-ltac2-dispatch branch from b071f71 to e721ac7 Compare March 29, 2026 18:35

rlepigre-skylabs-ai reviewed Mar 30, 2026

View reviewed changes

	(libraries coq-core.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))
	(libraries rocq-runtime.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))

Conversation

gmalecha-at-skylabs commented Mar 26, 2026

Uh oh!

Uh oh!

Uh oh!

skylabs-ai-ci bot commented Mar 26, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Uh oh!

skylabs-ai-ci bot commented Mar 27, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

skylabs-ai-ci bot commented Mar 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci bot commented Mar 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

skylabs-ai-ci bot commented Mar 29, 2026

CI summary (Details)

Active Repos

Passive Repos

Performance

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Janno commented Mar 30, 2026

Uh oh!

gmalecha-at-skylabs commented Mar 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants