coq-library-undecidability icon indicating copy to clipboard operation
coq-library-undecidability copied to clipboard

Published 20 hours ago • verified publisher icon uds-psl

separated L extraction framework

Open mrhaandi opened this issue 4 months ago • 6 comments

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. https://github.com/coq/coq/pull/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.

mrhaandi avatar Oct 05 '24 10:10 mrhaandi