Enrico Tassi (Dec 02 2021 at 12:51): 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?
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...
Pierre-Marie Pédrot (Dec 02 2021 at 12:59):Wut. I had never seen that.
Enrico Tassi (Dec 02 2021 at 13:00):Me neither... but it is there...
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:
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
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):Not sure what it does
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
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 13:02):maybe we use the usual slot next week if @Enrico Tassi can
Enrico Tassi (Dec 02 2021 at 13:03):I'll do my best
Gaëtan Gilbert (Dec 02 2021 at 13:03):git history says it's from https://github.com/coq/coq/commit/f9261830d886bf08599921d42539d8651437303f
actually no
Gaëtan Gilbert (Dec 02 2021 at 13:04):https://github.com/coq/coq/commit/861ccf4dd736b911ba0149550e298ce9fddf4c80
which says Réintroduction so it existed previously
Gaëtan Gilbert (Dec 02 2021 at 13:11):not sure coqdep understands this stuff though
Last updated: Apr 16 2024 at 16:01 UTC