search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
137 stars 50 forks source link

No stdlib #681

Open patrick-nicodemus opened 1 month ago

patrick-nicodemus commented 1 month ago

This makes some changes throughout the build script to replace the automatic importing of the Prelude everywhere with an explicit, qualified importation, as part of an attempt to track down why Require Elpi has the effect of Require Prelude.

After changing the dune files it seems clear that we cannot remove the dependence on the Prelude without removing the dependence on the String module, so I will hold off on doing anything further until someone can suggest a workaround to using String in the build script.

gares commented 1 month ago

The string thing is a hack to work around a limitation in dune. I'll keep the pr open waiting for that to be fixed, there is a pr that will eventually be merged.

proux01 commented 2 weeks ago

Note that this may be related to https://github.com/coq/coq/pull/19530 I also made an attempt in that direction https://github.com/proux01/coq-elpi/tree/without_stdlib