What happened to `L`?

[JoJoDeveloping]

Currently, the entire development in the L folder is commented out. This is unfortunate, since coq-library-fol relies on it, for example here:

https://github.com/uds-psl/coq-library-fol/blob/b967df481c13e0fa2336051105a9629e935c7eb8/theories/Incompleteness/epf_mu.v#L9

What is the current status of the L development? In porting to 9.0, what can we expect to still be there and what might be removed?

[mrhaandi]

In master the L framework is not present because it relies on strictly more than rocq-prover.
In regular releases, coming 9.0 we will work on including and maintaining it, together with further dependencies such as coq and coq-metacoq-template.

[mrhaandi]

@JoJoDeveloping could you point out which statements from the L framework you require.
This would also help the discussion on #227

[mrhaandi]

@JoJoDeveloping
I took a loot at epf_mu.v. It does not seem to actually use the L framework. Rather, lemmas for mu-recusive functions are put together in one file with lemmas using the L framework.
I created a branch https://github.com/mrhaandi/coq-library-undecidability/tree/MuRec-eval which puts all murec functions you use in epf_mu.v into the file MuRec/Util/eval.v. Is this sufficient to build coq-library-fol? Are there other parts of coq-library-fol which actually require the L framework?

[JoJoDeveloping]

Is this sufficient to build coq-library-fol?

Yes!

Are there other parts of coq-library-fol which actually require the L framework?

No.

Thanks a lot for looking into it 🙂

[mrhaandi]

The refactoring is in master and the CI is also fixed.

[JoJoDeveloping]

That means this is solved 🎉