Stream: Coq devs & plugin devs

Topic: Better coqc


view this post on Zulip Ali Caglayan (May 11 2022 at 17:19):

So it was mentioned on the call today that it could be possible to make a coqc which doesn't use so much memory. AFAIOU today coqc is just a special case of coqtop, which means that it also does some stuff with the STM which isn't really needed during compilation.

view this post on Zulip Ali Caglayan (May 11 2022 at 17:19):

How might we go forward with this?

view this post on Zulip Ali Caglayan (May 17 2022 at 15:48):

ping @Pierre-Marie Pédrot

view this post on Zulip Pierre-Marie Pédrot (May 17 2022 at 16:13):

The code is already there somewhere on @Emilio Jesús Gallego Arias 's repo, the branch is called simple coqc or something.

view this post on Zulip Enrico Tassi (May 17 2022 at 17:50):

IIRC it is a bit too simple but it is a good starting point.


Last updated: Feb 05 2023 at 20:03 UTC