build-list.py: implicitly add _RocqProject targets corresponding to each file in the list

[simon-skylabs]

This changes build-list.py so that, when creating a dune.inc file, for each target it adds to the file, it looks up all the dune files that dominates that target and for each dune file that specifies a Rocq project, add a corresponding _RocqProject target to dune.inc.

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
./	simon/build-list-rocq-project	e5132c3	923d969	main	db1581e	#180

Passive Repos

Repo	Job Branch	Job Commit
fmdeps/BRiCk/	main	e819c36
fmdeps/auto/	main	4712f6c
fmdeps/auto-docs/	main	6490c5f
bluerock/NOVA/	skylabs-proof	f3533d2
bluerock/bhv/	skylabs-main	e37df58
fmdeps/brick-libcpp/	main	be863c8
fmdeps/ci/	main	e1ec839
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	227bb83
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	5c3d0ab
vendored/vsrocq/	skylabs-main	ee79e7a

No Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	91	0	0	91

Performance

Relative	Master	MR	Change	Filename
-0.00%	198166.7	198166.7	-0.0	total
-0.00%	53108.6	53108.6	-0.0	├ translation units
+0.00%	145058.2	145058.2	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-0.00%	198166.7	198166.7	-0.0	total
-0.00%	53108.6	53108.6	-0.0	├ translation units
+0.00%	145058.2	145058.2	+0.0	└ proofs and tests

[pgiarrusso-sl]

What does that _RocqProject target do?
But honestly, my feeling is I'd either keep things as they are or backport the dune patches.

[Janno]

What does that _RocqProject target do?

I assume it builds the _RocqProject file so that the user of build-list.py can actually step through the built files in PG.

But honestly, my feeling is I'd either keep things as they are or backport the dune patches.

I don't think I understand your reply. Adding explicit _RocqProject targets to the dune file generated by build-list.py is not subsumed by any dune patches I am aware of. When the @rocqproject alias lands, it is conceivable that the explicit target in this PR will be replaced by that. But even then it might be worthwhile to scope it to just those folders where files are actually built. This could help when parts of the worktree are not currently functional and dune b @rocqproject might fail because of that. So we would probably still need the logic in this PR.

[rlepigre-skylabs-ai]

I think we can solve this problem in a much simpler way:

diff --git a/dune b/dune
index c12240a..2edf95b 100644
--- a/dune
+++ b/dune
@@ -8,3 +8,8 @@
   (deps (:yml (glob_files *.yml)) (:script build-list.py))
   (action
    (system "./%{script} -o %{target} %{yml} --relative-to='../../dyn' --root=../.."))))
+
+(rule
+ (alias rocqproject)
+ (deps (glob_files_rec _RocqProject))
+ (action (progn)))

With this, dune build @rocqproject ensures that all the _RocqProject files are in place.

This is not perfect though, since the alias only works from the workspace root. But at least it can be part of what happens in make ast-prepare or whatever the appropriate target is.

[pgiarrusso-sl]

Ah, I thought dune b path/to/_RocqProject didn't work, but it does. @rlepigre-skylabs-ai please submit that PR, I would approve it.

[pgiarrusso-sl]

But even then it might be worthwhile to scope it to just those folders where files are actually built. This could help when parts of the worktree are not currently functional and dune b @rocqproject might fail because of that. So we would probably still need the logic in this PR.

dune b @some/path/rocqproject would work then.

[pgiarrusso-sl]

I don't think I understand your reply.

Let me rephrase: the PR has no testcases, I don't understand the PR code or description. Your comment helps!

Extend build-list.py: when adding a target to its "build goal", also include _RocqProject files appropriate to browsing the target.

The current PR text gives instead the implementation strategy.

[rlepigre-skylabs-ai]

But even then it might be worthwhile to scope it to just those folders where files are actually built. This could help when parts of the worktree are not currently functional and dune b @rocqproject might fail because of that. So we would probably still need the logic in this PR.

dune b @some/path/rocqproject would work then.

Not sure I'm following this discussion, but if the generation of a _RocqProject file fails, then it must be that the dune config is broken and so invoking pretty much any dune command would fail. All that is involved in generating those files is ingesting the dune configuration files and building the deps, which happens whenever dune gets invoked.

[Janno]

I see. I was probably thinking of rocq dep failing because of syntax errors but if that's not involved in _RocqProject we should be fine.

[pgiarrusso-sl]

Then, maybe build-list.py could just add @rocqproject to its output?

Or we just do nothing since _RocqProject files don't change that much, and close this PR?