Stream: Dune devs & users

Topic: ✔ Using a compiled library


view this post on Zulip Julin Shaji (Oct 15 2023 at 17:08):

I just compiled it and the .vo files are in the repo itself.
Would it be possible to use them without doing a make install?
I was apprehensive of using make install because I don't how to do uninstall if needed.

view this post on Zulip Julin Shaji (Oct 15 2023 at 17:10):

And I'm using coq from nix.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:11):

In that case things could work if you set COQPATH=/location/of/mathcomp/

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:12):

Dune will look for installed libraries first using coqc -config, but extra search paths can be added using COQPATH

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:13):

so export COQPATH=/path/to/mathcomp:$COQPATH should work, note that you should point COQPATH to the root of mathcomp, so library mathcomp.ssreflect.seq for example is found in COQPATH/mathcomp/ssreflect/seq.vo

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:18):

Note that this should work in both (lang coq 0.8) and lower, but your theory file will be different.

In lang coq < 0.8, everything in COQPATH and user-contrib is in scope, auto-added by coqc, and not managed by dune.

In (lang coq 0.8) and newer, Dune manages the libraries too, so you need to add them to (theories ).

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:28):

Since this is in Nix, would you have to extend COQPATH rather than set it? You can check the COQPATH that Nix gives you to be sure

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:29):

Indeed, edited to reflect better practice

view this post on Zulip Julin Shaji (Oct 15 2023 at 17:30):

Oh yeah..

There was already something there:

$ echo $COQPATH
/nix/store/01m12mdg809y1819zpdl0p94d0wssgah-coq8.16-hierarchy-builder-1.4.0/lib/coq/8.16/user-contrib/:/nix/store/f93lwhhsqms0v1n0y5xblmrd7qrh1ds7-coq8.16-elpi-1.15.6/lib/coq/8.16/user-contrib/

Thanks!

view this post on Zulip Julin Shaji (Oct 15 2023 at 17:30):

It worked.

view this post on Zulip Notification Bot (Oct 15 2023 at 17:36):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:36):

But remember that env variables are local to a running shell and its children, so this won't survive a reboot or even opening a new terminal

view this post on Zulip Julin Shaji (Oct 15 2023 at 17:38):

Yeah, so the variable has to be set everytime. Got it.

view this post on Zulip Paolo Giarrusso (Oct 15 2023 at 17:38):

and subprocesses can override them, so this might break in nested nix-shell — it probably will in pure shells since they reset lots of the environment? (Not certain on this specific var)

view this post on Zulip Julin Shaji (Oct 15 2023 at 17:39):

Paolo Giarrusso said:

and subprocesses can override them, so this might break in nested nix-shell

Ah.. that's something to watch out for. :+1:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:40):

You can dispose the variable by vendoring math-comp , but the dune files for math-comp are not yet in the main repos c.f. https://github.com/math-comp/math-comp/pull/316

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2023 at 17:40):

But that can be a strategy that yields some interesting advantages too


Last updated: May 25 2024 at 20:01 UTC