Add coq.env.add-context for inserting context declarations

[VojtechStep]

There was no way to add implicit section variables, so context-decl objects could not be faithfully spliced from outside code.

I'd appreciate a naming suggestion for what I temporarily called coq.env.add-section-variable-two.

[gares]

Thanks, it looks good.

[gares]

I would be tempted to break the existing api, giving a default value to the argument when omitted.

Surely HB will need adjustment.
Would you mind trying and see what CI does discover?

[VojtechStep]

Would you mind trying and see what CI does discover?

I can try tomorrow.

[gares]

For the failure in master (nix) CC @CohenCyril

[gares]

Also, I forgot: here an example of an argument with a default (MP):

coq-elpi/src/coq_elpi_builtins.ml

Lines 1870 to 1878 in ee28024

	MLCode(Pred("coq.env.dependencies",
	In(gref, "GR",
	In(B.unspec modpath, "MP",
	Out(gref_set, "Deps",
	Read(unit_ctx, "Computes the direct dependencies of GR. If MP is given, Deps only contains grefs from that module")))),
	(fun root inside _ ~depth _ _ state ->
	let inside = unspec2opt inside in
	!: (dep1 ?inside (get_sigma state) root))),
	DocAbove);

[CohenCyril]

I would be tempted to break the existing api, giving a default value to the argument when omitted.

How about using an optional

• @implicit! => coq.env.add-section-variable Name Ty C
• @maximal! => coq.env.add-section-variable Name Ty C
• @explicit! => coq.env.add-section-variable Name Ty C

to preserve backward compat?

[gares]

That is also an option, but I'm not super fan of adding an attribute that is used only by one API.

As expected HB failed. @VojtechStep do you need guidance on how to have CI use a patched branch of HB?

[VojtechStep]

I wanted to make my local checkout of HB use this branch of coq-elpi, but I'm struggling to get it set up. I tried overriding HB's bundles."coq-8.20".coqPackages.coq-elpi.override.version with "#737", "/absolute/path/string/to/local/coq-elpi", ../nix/path/object/to/local/coq-elpi and import ../coq-elpi {}, but no luck so far.
The first and third ones fail with unbound symbols (e.g. Unbound module Elpi.API.Ast.Scope in File "src/coq_elpi_HOAS.mli", line 160, characters 14-41).
The second with "do not know how to unpack source archive /absolute/path/..." (kind of as expected).
The fourth one fails with "function default-fetcher called without required argument rev" in build-support/coq/meta-fetch/default.nix.

Any help would be appreciated.

[VojtechStep]

I also tried adding bundles."coq-8.20".ocamlPackages.elpi.override.version = "2.0.6";, which didn't have any effect — even elpi --version in a new nix-shell still gives 1.19.2.

[gares]

I also tried adding bundles."coq-8.20".ocamlPackages.elpi.override.version = "2.0.6";, which didn't have any effect — even elpi --version in a new nix-shell still gives 1.19.2.

This is a known issue, but I don't know the solution while @CohenCyril does

[CohenCyril]

Ah yeah, I did a stupid mistake somewhere and we keep bumping into it...
The override for elpi is in the derivation of coq-elpi (instead of the general scope of coq packages 😕 ) see e.g. this commit to see where it is overriden f51d2c5

so sorry about that.

[VojtechStep]

No worries, I figured it out in the meantime 👌

[gares]

It seems HB is the only package impacted by the change, so I think this patch is fine.
I'll try to see how to make HB compile with 2.3.0 and also with this change.

[gares]

waiting ocaml/opam-repository#27258

[gares]

I tried to make nix build against the upstream PR and tag but I failed.
I guess I'll wait for a proper release...