Stream: Coq devs & plugin devs

Topic: expand_path_macros


view this post on Zulip Enrico Tassi (Dec 02 2021 at 12:51):

I've just noticed this (clunky) piece of code https://github.com/coq/coq/blob/master/lib/envars.ml#L69 which is called to pre-process the argument to AddLoadPath but also DeclareMLModule.

Is this documented? Can I use it to make backward compatible overlays for #15220?

view this post on Zulip Enrico Tassi (Dec 02 2021 at 12:51):

It seem to let me write Declare ML Module "$FOO" and get the value of FOO from the environment...

view this post on Zulip Pierre-Marie Pédrot (Dec 02 2021 at 12:59):

Wut. I had never seen that.

view this post on Zulip Enrico Tassi (Dec 02 2021 at 13:00):

Me neither... but it is there...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 13:01):

I have seen this stuff before, I thought you had introduced it :joy: :joy:

view this post on Zulip Gaëtan Gilbert (Dec 02 2021 at 13:01):

we just need to put $COQ_VERSION in the environment, then people can Load "foo_$COQ_VERSION" to get version dependent code

view this post on Zulip Enrico Tassi (Dec 02 2021 at 13:01):

Anyway, it would help me only in one case, so it is not a life changer... we well keep it for a trivia night

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):

Not sure what it does

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):

Gaëtan Gilbert said:

we just need to put $COQ_VERSION in the environment, then people can Load "foo_$COQ_VERSION" to get version dependent code

The best of all wolrds XDDD

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):

By the way François Bobot said he would be very happy to meet to see how we can patch dune

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):

maybe we use the usual slot next week if @Enrico Tassi can

view this post on Zulip Enrico Tassi (Dec 02 2021 at 13:03):

I'll do my best

view this post on Zulip Gaëtan Gilbert (Dec 02 2021 at 13:03):

git history says it's from https://github.com/coq/coq/commit/f9261830d886bf08599921d42539d8651437303f
actually no

view this post on Zulip Gaëtan Gilbert (Dec 02 2021 at 13:04):

https://github.com/coq/coq/commit/861ccf4dd736b911ba0149550e298ce9fddf4c80
which says Réintroduction so it existed previously

view this post on Zulip Gaëtan Gilbert (Dec 02 2021 at 13:11):

not sure coqdep understands this stuff though


Last updated: Feb 01 2023 at 16:03 UTC