[vernac] expose API to elaborate declarations

[gares]

In the context of Elpi I want to let coq elaborate an inductive declaration (up to the constr level) without necessarily adding it to the environment, the same for records and context.
This PR exports the first half of do_mutual_inductive (the part which is side effect free) and do_record and do_context.

Fixes #14737

TODO:

• overlay for coq-elpi using the new API

[ejgallego]

Modulo the two nits this looks good to me.

[ejgallego]

LGTM, @gares I assume you want to wait for the overlay, so I will wait to merge.

[gares]

I'm not sure the code the last commit exposes is in the right place. Happy to move it elsewhere, just tell me where.
I did hoist ".glob handling" since that part has nothing to do with pre-processing (which clients may want to call without necessarily emitting glob data).

[gares]

So, after more work on the overlay (which is not ready yet, but is converging), the exposed API is:

• pre processing of the data carried by VernacInductive, which gives two distinct ASTs: inductive or record
• elaboration of inductive
• elaboration of record

The latter one has a very nasty type, suggestions are welcome.

The overall feeling is that having just one VernacInductive node is wrong, since one later has to unshare options/flags, and finally take two very different code paths. But that would be another PR (changing the grammar). The funny thing is that the grammar entries for records and general inductive shares almost nothing already, and the two productions are easy for an LL parser, since it is the first word that choose (Record & co, vs Inductive & co). So I really don't get why the code is done this way.

[ejgallego]

Thanks @gares will have a deeper look when the overlay is ready, but indeed I agree with your comments, we can do a lot of improvements in this area. For sure this PR will improve things already.

[gares]

I'm almost done with the overlay, sorry for taking so long, but it was not trivial. So far the API is sufficient, but I'm not done.

[ejgallego]

I'm almost done with the overlay, sorry for taking so long, but it was not trivial. So far the API is sufficient, but I'm not done.

No worries at all take your time!

[coqbot-app]

🔴 CI failure at commit f2ad35d without any failure in the test-suite

✔️ Corresponding job for the base commit f9c9ee5 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-analysis

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failure at commit f2ad35d without any failure in the test-suite

✔️ Corresponding job for the base commit f9c9ee5 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-analysis

• You can also pass me a specific list of targets to minimize as arguments.

[gares]

fiat failure seems unrelated. I can't say about analysis.

[coqbot-app]

🔴 CI failure at commit f2ad35d without any failure in the test-suite

✔️ Corresponding job for the base commit f9c9ee5 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-analysis

• You can also pass me a specific list of targets to minimize as arguments.

[gares]

CI was green but for fiat which is fixed in master, so I did rebase to get a fully green CI.
After that, please merge.

[gares]

@SkySkimmer would you mind taking care of this? I'd like to first merge this elpi overlay, and then prepare the one for #15946

[SkySkimmer]

@ejgallego is still assigned though

[Alizter]

@SkySkimmer I think it is OK to take over in this case. The assignment was a month ago, so I don't think we can reasonably expect it to be looked at.

[SkySkimmer]

Last activity was just before holidays though

[gares]

I think @ejgallego was OK with the PR both in principle and with the current code, I did only add a few comments after his review.

[ejgallego]

The assignment was a month ago, so I don't think we can reasonably expect it to be looked at.

I am not sure why, my last activity was 11 days ago, then I went on holidays [and I did a review but the PR was not ready, so really I could only have reacted on the weekend] . So yes, the assignement date is one month, but how it is relevant?

That being said, the PR looks good to me, so go ahead and take over. A think to keep in mind tho is the conflict with #15877 , that one I did have a look but I didn't manage to understand the code. I'd suggest pinging @proux01 in case he'd like to comment anything about this one.

[gares]

If you are back from VAC you can also merge it yourself. I'd like to merge overlay, since I then have to make another one which will generate conflicts, so a quick merge would be appreciated

[SkySkimmer]

@coqbot merge now

[coqbot-app]

@SkySkimmer: Please take care of the following overlays:

• 15872-gares-interp-inductive.sh

[gares]

thanks