Stream: Coq devs & plugin devs

Topic: coqide vs findlib


view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 12:42):

is the bug mentioned in https://github.com/coq/coq/commit/870d81c699b5d15420a03f2006a7938a158c09a8 reopened?

view this post on Zulip Enrico Tassi (Feb 09 2022 at 13:18):

It depends if the load paths are now part of the summary or not (at that time, they were not)

view this post on Zulip Enrico Tassi (Feb 09 2022 at 13:19):

I believe they should, otherwise Undo has no effect on that command

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 13:25):

but we link plugins before we unfreeze the normal summaries so how does it matter if the loadpath is in the summary?

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 13:25):

https://github.com/coq/coq/blob/68b485ff65da34764016e8e1b2570e9d20f7566c/library/summary.ml#L81-L86

view this post on Zulip Enrico Tassi (Feb 09 2022 at 13:38):

Right, so one more reason to ditch Add LoadPath


Last updated: Feb 06 2023 at 19:03 UTC