Stream: Coq devs & plugin devs

Topic: Add LoadPath vs Add Rec Loadpath


view this post on Zulip Arpan Agrawal (Jan 02 2024 at 17:51):

I'm porting a Coq plugin from 8.11 to 8.12, and I understand that loadpaths now need to be qualified with a library name. Is there a difference between "Add Loadpath ... as Foo", "From Foo Require Import" vs "Add Rec Loadpath", "Require Import"

Also, what is the suggested way of making this change in the _CoqProject file, so I dont have to make the change in each file individually?
Thanks!

view this post on Zulip Gaëtan Gilbert (Jan 02 2024 at 20:12):

use -Q or -R in the coqproject

view this post on Zulip Arpan Agrawal (Jan 02 2024 at 20:23):

I did try using -R in the coqproject (I added a new line that says -R coq Foo, where coq is the folder where I want to import from). But I still need to change the imports to "From Foo Import ..." in each individual file, is that correct?

view this post on Zulip Gaëtan Gilbert (Jan 02 2024 at 20:29):

with -Q yes, with -R no


Last updated: Oct 13 2024 at 01:02 UTC