separated L extraction framework

[mrhaandi]

Currently, no undecidability and computability result strictly depends on the L extraction framework. In order to improve maintainability of the library, the L extraction framework is moved to a separate project https://github.com/uds-psl/L-extraction.
Moving the framework removes the coq-metacoq-template dependency, making coq the only dependency.
This may enable a reinclusion of coq-library-undecidability into Coq CI, cf. coq/coq#19339

This depends from metacoq and it appears it is not tested in metacoq CI, which means any change in metacoq could subrepticly break the CI here.

@yforster @dominik-kirst @DmxLarchey feel free to comment.

[yforster]

As I said on the other PR:

I'd not like to drop the reduction relying on the framework completely from the code to keep the framework alive

Now moving the framework to another repo just means we have to maintain two things, and we buy a dependency in the library once a proof uses a framework.

So overall, I think this doesn't improve the situation.

[mrhaandi]

Now moving the framework to another repo just means we have to maintain two things.

If removing a coq-metacoq-template dependency can get coq-library-undecidability back into Coq CI (which is my main motivation), then we actually need to maintain only one thing (the extraction framework, without too much commitment).
Several weeks ago Coq master broke the undecidability library and it took me quite some effort to get it working again.

and we buy a dependency in the library once a proof uses a framework.

For _undec results there is no reason to reduce anything to L, so I do not see how the extraction framework will be of importance in the future. One aspect could be to show RE membership, which is not what we usually are interested in mechanizing.

So overall, I think this doesn't improve the situation.

Do you have some suggestions on how to improve the situation?

[mrhaandi]

From my perspective, it would be a good situation to have coq-library-undecidablity in Coq CI and L-extraction in metacoq CI.

[DmxLarchey]

If I understand well, there are two conflicting issues here:

1. one issue with the L extraction framework is its dependency with MetaCoq which possibly or actually hinders the synchronization between Coq and the undecidability library;
2. another issue is maintaining the L extraction framework which could possibly become outdated if its update is not required by its inclusion in the undecidability library.

One of the principle we discussed in the earlier days was to not depend heavily on external libraries, precisely to avoid synchronization issues like item 1, and rather include the necessary source code inside the undecidability lib. I found and still find this is a good principle. I do not know if it is applicable to L-extraction but I doubt it.

On the other hand, I understand that moving L extraction out could possibly mean that in the end, it becomes deprecated, if nobody finds the necessity (or will) to maintain it.

Since L extraction was an important contribution of the library, it is hard to view it as an external library. So this question is hard to solve.

@yforster seem to think it is possible/likely that at some point, a new undecidability target might use the L extraction framework, and then create a dependency on that and hence MetaCoq again.

I did not heavily review that L extraction code, so I do not know if an external contribution is very likely. It is usually hard to enter the code of someone else unless heavily tipped.

Would the last proposition of @mrhaandi, putting L-extraction in the MetaCoq CI, solve the issue 2 of its maintenance ? May be I miss some other issue.

[yforster]

The removal from Coq's CI was, if I remember correctly, also mainly because we are a pure library and do not provide test coverage that other projects don't provide. So I doubt that we'll be reintegrated, so we're back to the state every other Coq project has: We have to keep up with Coq's master.

In the modern days, synchronisation is not a major issue anymore. There's the Coq platform, opam packages are usually relased quickly (MetaCoq was already released when I looked at releasing for Coq 8.20).

So in short: I think we're trying to fix a hypothetical future issue here that doesn't exist.

(There is no MetaCoq CI because there is no good way in Coq to do "forward" CI. So we can't put L extraction there.)

[mrhaandi]

According to the Zulip discussion we may get back into the Coq CI if we had no dependencies.
Since reverting this particular PR is easy, we can at least try.