r-muhairi (Feb 17 2023 at 02:39): r-muhairi (Feb 17 2023 at 02:39):Hi @Ali Caglayan
I think there is an issue with how nix packages Coq, its just a single derivation for some reason. Even the coq source packages coq as a single derivation? I'm not sure i haven't looked at the nix coq infra in a very long time
Removing the submodules would mean we'll be building coq quite regularly which isn't ideal despite us not actually needing coq as a dependency, but instead the ocaml libraries provided, say coq-core and so on.
I may be misunderstanding something here, if not I'll look into packaging what we actually need from Coq first. Thankfully, coq (unlike ocaml :sad: ) switched to dune awhile back which should make it quite straightforward
Ali Caglayan (Feb 17 2023 at 02:41):Yes, we don't need the actual Coq binary, just the libraries it uses.
Ali Caglayan (Feb 17 2023 at 02:41):Which make up the binary.
r-muhairi (Feb 17 2023 at 02:42):In either-case, yeah I don't think it even built when I tried overriding the coq source for some reason
Ali Caglayan (Feb 17 2023 at 02:42):The nix derivation for coq is using ocaml 4.12 but for some reason I cannot get that to propogate
Ali Caglayan (Feb 17 2023 at 02:42):If that doesn't propgate things like findlib will not find the coq libraries when building with Dune
r-muhairi (Feb 17 2023 at 02:43):Ali Caglayan said:
The nix derivation for coq is using ocaml 4.12 but for some reason I cannot get that to propogate
Yeah nixpkgs is really behind, i'll look into separately creating multiple derivations directly from the coq source, and see if what they have currently could alleviate the need for maintenance overtime
Ali Caglayan (Feb 17 2023 at 02:46):Coq source also has it's own derivation which could be used
r-muhairi (Feb 17 2023 at 02:47):Ali Caglayan said:
Coq source also has it's own derivation which could be used
Unfortunately not,just looked over the nix expression
looks like it is a single-derivation of the entire codebase? Now that needs a PR :angry:
https://github.com/coq/coq/blob/master/default.nix
Ali Caglayan (Feb 17 2023 at 02:48):Our Nix maintainers only do what is necessary and don't have an abundance of time so PRs are always welcome
Ali Caglayan (Feb 17 2023 at 02:49):The nix infra for Coq is geared towards fixing coq and instaliing coq libraries along side
Ali Caglayan (Feb 17 2023 at 02:49):For which it is great.
Ali Caglayan (Feb 17 2023 at 02:49):But nix derivations exposing internal libraries are lacking
Ali Caglayan (Feb 17 2023 at 02:49):mostly because Coq recently switched to Dune and that story was not easily attainable before
r-muhairi (Feb 17 2023 at 02:49):I can see that, i understand
I was working on something that'll alleviate the pain of managing nix infrastructure for non-nix first coq/ocaml teams
but unfortunately it isn't ready yet
Ali Caglayan (Feb 17 2023 at 02:53):That sounds wonderful :)
Ali Caglayan (Feb 17 2023 at 02:54):Here is a project that has a lot of users based on the current nix infra: https://github.com/coq-community/coq-nix-toolbox
Ali Caglayan (Feb 17 2023 at 02:54):It is my hope that we can make this kind of thing easier to maintain
Ali Caglayan (Feb 17 2023 at 02:55):and more composable etc.
Ali Caglayan (Feb 17 2023 at 02:56):One user facing feature that is popular there is the generation of github actions workflows
Ali Caglayan (Feb 17 2023 at 02:56):in theory this could all be done with flakes, but this came before and works
Ali Caglayan (Feb 17 2023 at 02:56):and flakes are still considered experimental (i think)
Ali Caglayan (Feb 17 2023 at 02:57):The story for compiling against coq libraries was always difficult AFAIK
Ali Caglayan (Feb 17 2023 at 02:57):But as I said, has gotten easier, we just need ot make the right improvements
r-muhairi (Feb 17 2023 at 02:57):I mean what I was working on was exposing bunch of custom nix expressions, along the lines of a ocaml/coq mkDerivation, buildDunePackageand so on. Exposing a nix-first automated opam index similar to nixpkgs with support for previous versions/conflicts and have an optional cli to generate nix expressions from opam files and vice-versa using nix eval.
Ali Caglayan (Feb 17 2023 at 02:58):Yes being able to derive from opam packing would be great
Ali Caglayan (Feb 17 2023 at 02:59):There are already quite a few projects that do this for ocaml such as opam-nix, nix overlays etc.
Ali Caglayan (Feb 17 2023 at 02:59):But Coq's setup with the libraries always typically breaks
r-muhairi (Feb 17 2023 at 02:59):Ali Caglayan said:
There are already quite a few projects that do this for ocaml such as opam-nix, nix overlays etc.
I have so many faults with every existing nix solution, especially opam-nix
Ali Caglayan (Feb 17 2023 at 03:00):There are quite a few issues with opam nix I agree. But for simple OCaml projects it works pretty good.
r-muhairi (Feb 17 2023 at 03:00):nix-overlays is a small set of manually packaged ocaml packages
r-muhairi (Feb 17 2023 at 03:00):it is only a solution if all what you need is there
Ali Caglayan (Feb 17 2023 at 03:01):Yes
r-muhairi (Feb 17 2023 at 03:02):Ali Caglayan said:
There are quite a few issues with opam nix I agree. But for simple OCaml projects it works pretty good.
No, not at all
I've tried it personally multiple times out of frustration and I was disappointed each time with how slow it is, and what it does plus the fact it relies on IFD
And the limitations imposed by how its designed
Ali Caglayan (Feb 17 2023 at 03:02):It is slow and does terrible use. But it is used in projects like Dune and ocaml-lsp. At least for the dev shells.
r-muhairi (Feb 17 2023 at 03:02):Calling out onto opam was such a bad decision
Ali Caglayan (Feb 17 2023 at 03:03):Yes, IIRC this predated Dune use however.
Ali Caglayan (Feb 17 2023 at 03:03):We could do much smarter things knowing we have Dune projects.
Ali Caglayan (Feb 17 2023 at 03:03):For OCaml and Coq alike
r-muhairi (Feb 17 2023 at 03:03):Ali Caglayan said:
It is slow and does terrible use. But it is used in projects like Dune and ocaml-lsp. At least for the dev shells.
yeah thats unfortunate
Ali Caglayan (Feb 17 2023 at 03:04):The issue is the same as always, Nix requires some knowledge to get things right, and most people don't have that time.
r-muhairi (Feb 17 2023 at 03:04):I mean lets just hope what i'm working on turns out well, which from the looks of things it is going well :)
A nix-first, pure solution towards encompassing the OCaml & Coq ecosystems into nix.
Ali Caglayan (Feb 17 2023 at 03:05):I look forward to hearing your progress :)
r-muhairi (Feb 17 2023 at 03:06):Anyhow back to the topic
I'll start when i get free time working on getting the libraries we need out of the coq source as separate derivations
Ali Caglayan (Feb 17 2023 at 03:07):Sounds good, keep me in the loop :)
r-muhairi (Feb 18 2023 at 02:52):Got it to build without relying on coqPackages, creating a derivation only for coq-core
i'll open a PR to your branch now
edit: https://github.com/Alizter/coq-lsp/pull/1
r-muhairi (Feb 19 2023 at 03:16):@Ali Caglayan FYI, it doesn't build with HEAD, fails with coq-serapi
Ali Caglayan (Feb 19 2023 at 03:18):You mean it is failing with the latest serapi?
r-muhairi (Feb 19 2023 at 03:18):Yeah
Ali Caglayan (Feb 19 2023 at 03:18):That shouldn't happen, @Emilio Jesús Gallego Arias can you take a look?
Ali Caglayan (Feb 19 2023 at 03:19):Huh I guess you need to bump the coq version too
Ali Caglayan (Feb 19 2023 at 03:20):most likely serapi had an overlay merged but coq is stuck in the past
Ali Caglayan (Feb 19 2023 at 03:20):When Coq breaks a development like serapi, they will submit overlays for them to be merged.
r-muhairi (Feb 19 2023 at 03:20):Also, I tried using coq-lsp built at that point however i'm getting this error, I don't have coq installed in the current env so that may be the reason, but the error isn't clear on that end image.png
Ali Caglayan (Feb 19 2023 at 03:22):What did you have in your buffer?
r-muhairi (Feb 19 2023 at 03:24):Ali Caglayan said:
What did you have in your buffer?
It's in every example in the examples directory
Ali Caglayan (Feb 19 2023 at 03:25):ah, we need to install the coq standard library of course
Ali Caglayan (Feb 19 2023 at 03:25):we only provided coq-core with the flake
r-muhairi (Feb 19 2023 at 03:25):Ali Caglayan said:
we only provided coq-core with the flake
ic, i'll add a separate derivation to the devShell
Ali Caglayan (Feb 19 2023 at 03:30):@r-muhairi btw you can push directly to my PR
Ali Caglayan (Feb 19 2023 at 03:31):ah nevermind it looks like github requires write access for that
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:46):That error seems pretty weird! @r-muhairi can you enable the coq-lsp.debug option?
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:46):Basically that's the assertion you are getting
let start_library dir senv =
(* When starting a library, the current environment should be initial
i.e. only composed of Require's *)
(* XXX is it really possible / should be allowed to have nonempty Requires?
especially if [dir] is in the [senv.required] *)
assert (is_initial senv);
assert (not (DirPath.is_empty dir));
Fleche.Doc.create, internal error: Anomaly
"File "kernel/safe_typing.ml", line 1272, characters 2-8: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Safe_typing.start_library in file "kernel/safe_typing.ml", line 1272, characters 2-26
Called from Global.globalize in file "library/global.ml", line 56, characters 16-31
Called from Declaremods.start_library in file "vernac/declaremods.ml", line 719, characters 11-35
Called from Coq__Workspace.apply in file "coq/workspace.ml", line 167, characters 2-49
Called from Coq__Init.doc_init in file "coq/init.ml", line 82, characters 2-32
Called from Coq__Protect.eval_exn in file "coq/protect.ml", line 38, characters 14-17
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:52):I'm super puzzled, I don't understand how this error could ever happen; what coq and coq-lsp commit hash you have?
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:52):Ali Caglayan said:
Huh I guess you need to bump the coq version too
Yes for main coq and coq-serapi have to be in sync :S
r-muhairi (Feb 19 2023 at 03:57):Emilio Jesús Gallego Arias said:
I'm super puzzled, I don't understand how this error could ever happen; what coq and coq-lsp commit hash you have?
Good thing this error arose from the nix build, easily reproducible haha
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:59)::rolling_on_the_floor_laughing:
Emilio Jesús Gallego Arias (Feb 19 2023 at 03:59):Whatever error is this one, it is gonna a fun one
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:13):Note that the commit you point out didn't exits on my repos, maybe that was the problem?
r-muhairi (Feb 19 2023 at 04:18):Emilio Jesús Gallego Arias said:
Note that the commit you point out didn't exits on my repos, maybe that was the problem?
The flake inputs?
r-muhairi (Feb 19 2023 at 04:22):Actually, if i recall correctly I went back and tried to build with submodules and still had the same error so it may just be the fact stdlib is missing
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:47):That could be, however I wonder how that condition triggers that error.
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:48):if coq-stdlib is missing you should get
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:48):(deleted)
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:48):Fleche.Doc.create, internal error: Cannot find a physical path bound to
logical path Coq.Init.Prelude.
That assert in the kernel is super strange to trigger, first thing we do before setting up anything, we save the root_state which contains an empty env
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:50):so how initial_env can fail is beyond my understanding
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:51):Let's see if Ali can reproduce
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:52):@r-muhairi do you have the LSP trace of the server?
Emilio Jesús Gallego Arias (Feb 19 2023 at 04:52):by setting Coq-LSP > Trace to Messages?
r-muhairi (Feb 19 2023 at 05:18):Emilio Jesús Gallego Arias said:
Fleche.Doc.create, internal error: Cannot find a physical path bound to logical path Coq.Init.Prelude.
I do get this error as well, but in some files and in others the assertion error
r-muhairi (Feb 19 2023 at 05:23):Output
r-muhairi (Feb 19 2023 at 05:25):ops i may have messed up something with coq-core's derivation because coqlib is pointed at a directory that doesn't exist
r-muhairi (Feb 19 2023 at 05:30):which isn't meant to be using the coq-core's derivation in the first place..? Ah
r-muhairi (Feb 19 2023 at 05:43):Which seems to still be relying on the coq-core's derivation out as opposed to coq's even when i pass that
@Emilio Jesús Gallego Arias do you know how COQLIB is set/inferred?
r-muhairi (Feb 19 2023 at 05:44):i assume its an env variable let me try setting it explicitly
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:44):Aha, I see the problem now, very interesting (and bug in Coq's upstream error handling I think)
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:45):As of today coqlib is set at configure time
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:45):coq-lsp won't recognize the env variable, but maybe we should add that?
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:46):you can also set --coqlib in the command line arguments
r-muhairi (Feb 19 2023 at 05:47):ok this is confusing
r-muhairi (Feb 19 2023 at 05:47):
r-muhairi (Feb 19 2023 at 05:49):in this case it may be appropriate to produce a symLinkJoin derivation with coq-core because of how it's accessing /lib/coq-core
why is it doing that anyhow
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:54):it is assuming that lib/coq and lib/coq-core live in the same directory
r-muhairi (Feb 19 2023 at 05:55):Emilio Jesús Gallego Arias said:
it is assuming that
lib/coqandlib/coq-corelive in the same directory
thats weird behavior
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:56):it is indeed weird
Emilio Jesús Gallego Arias (Feb 19 2023 at 05:59):@r-muhairi so that I understand, you are folks doing the coq-core split
r-muhairi (Feb 19 2023 at 06:00):Emilio Jesús Gallego Arias said:
r-muhairi so that I understand, you are folks doing the coq-core split
yeah as thats what coq-lsp needs, that worked fine
r-muhairi (Feb 19 2023 at 06:01):just being able to use coq now so we can actually use coq-lsp at that specific point for say testing
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:01):I see
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:01):so indeed what Coq is doing won't work well for nix
r-muhairi (Feb 19 2023 at 06:01):yeah, we can't have separate derivations like this
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:02):so in the one package setup, -prefix sets the coqlib
r-muhairi (Feb 19 2023 at 06:02):but we can just build coq with coq-core as opposed to having separate derivations in that case however that isn't really ideal
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:02):let's fix this
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:02):the question is how do you want to pass the lib/coq-core path
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:02):I can do a patch
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:03):to try to auto-detect it
r-muhairi (Feb 19 2023 at 06:03):its probably better to introduce a new env say $COQCORE as opposed to expect $COQLIB to have coq-core in the same directory
r-muhairi (Feb 19 2023 at 06:04):or from nix's side we can have coq-core same directory by linking
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:04):what does ocamlfind query coq-core say in Nix?
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:04):Coq can use that to locate coq-core
r-muhairi (Feb 19 2023 at 06:04):/nix/store/83ah3xhjl0rz6vfvzvbvj5kailz1lx2h-ocaml4.14.0-coq-core-20230215132751+8.18+alpha/lib/ocaml/4.14.0/site-lib/coq-core
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:05):is that the right path?
r-muhairi (Feb 19 2023 at 06:05):not exactly
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:05):Oh
r-muhairi (Feb 19 2023 at 06:05):actually, yes it is
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:05):Good, then I will patch coq-lsp to use that
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:05):that patch should be put into Coq too
r-muhairi (Feb 19 2023 at 06:05):its symlink of /lib/coq-core
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:06):IMHO no need to add a variable
r-muhairi (Feb 19 2023 at 06:06):agreed
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:06):as ocamlfind should be properly configured as for Coq to work
r-muhairi (Feb 19 2023 at 06:06):yeah
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:10):The error you had should be now fixed in main
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:10):it should now complain just about not finding init.prelude
Emilio Jesús Gallego Arias (Feb 19 2023 at 06:10):and the wrong coq-core dir
r-muhairi (Feb 19 2023 at 07:30):@Emilio Jesús Gallego Arias fyi there is COQCORELIB
r-muhairi (Feb 19 2023 at 08:09):(deleted)
r-muhairi (Feb 19 2023 at 08:22):(deleted)
r-muhairi (Feb 19 2023 at 08:33):aye! got it to work
Ali Caglayan (Feb 19 2023 at 14:03):Yes, I had noticed the Coq hack to get to coq-core before. It won't work when coq-core and coq are not in teh same directory.
Ali Caglayan (Feb 19 2023 at 14:03):I think if COQCORELIB is not explicitly configured then it is guess as $COQLIB/../coq-core
r-muhairi (Feb 19 2023 at 14:32):That aside, i find it problematic that we're creating our own derivations for coq, especially since 8.18+alpha isn't upstreamed so people can't actually use it
but i guess they can just pin the flake at a specific tag then
say 0.1.5+8.17
r-muhairi (Feb 19 2023 at 14:32):and we're using a separate coq source
r-muhairi (Feb 19 2023 at 14:33):Ali Caglayan said:
Yes, I had noticed the Coq hack to get to coq-core before. It won't work when
coq-coreandcoqare not in teh same directory.
all what i had to do is build the stdlib and create a coq-lsp wrapper passing a flag --coqlib to coq-stdlib/lib/coq
r-muhairi (Feb 19 2023 at 14:34):and expose COQCORELIB in a shellHook to $coq-core/lib/coq-core
r-muhairi (Feb 19 2023 at 14:34):which isn't ideal obviously, coqlib should be inferred through the env
r-muhairi (Feb 19 2023 at 14:35):i think the issue here is that coq-lsp is using coq-core to actually get the path to COQLIB if im not mistaken, somehow? But COQLIB is only there from coq-stdlib however coq-lsp doesn't depend on coq-stdlib, to build at least
and even then passing coq-stdlib as opposed to coq-core which depends on coq-core will still have coqlib at the coq-core derivation outpath
r-muhairi (Feb 19 2023 at 14:41):(deleted) just a direnv issue
Ali Caglayan (Feb 19 2023 at 14:50):The coqlib detection code in coq is a little bonkers, but here it is: https://github.com/coq/coq/blob/master/boot/env.ml
Ali Caglayan (Feb 19 2023 at 14:52):r-muhairi said:
Ali Caglayan said:
Yes, I had noticed the Coq hack to get to coq-core before. It won't work when
coq-coreandcoqare not in teh same directory.all what i had to do is build the stdlib and create a coq-lsp wrapper passing a flag --coqlib to coq-stdlib/lib/coq
I meant that Coq itself is using a hack to find it
r-muhairi (Feb 19 2023 at 14:52):Ali Caglayan said:
The coqlib detection code in coq is a little bonkers, but here it is: https://github.com/coq/coq/blob/master/boot/env.ml
how does coqc find coq-stdlib if installed with opam
Ali Caglayan (Feb 19 2023 at 14:54):I believe they are all installed in lib/coq for opam
Ali Caglayan (Feb 19 2023 at 14:56):One thing I am trying to understand is that if a user has Coq available via Nix, are we able to plug the sources into the flake?
Ali Caglayan (Feb 19 2023 at 14:56):Because if the coq-core versions are not matching, then we will run into trouble.
Ali Caglayan (Feb 19 2023 at 14:56):And if we are only building the stdlib for getting a working coq-core I believe there are some smarter things we can do.
Ali Caglayan (Feb 19 2023 at 14:57):But I'll let @Emilio Jesús Gallego Arias fill you in on that since my knowledge about this is quite patchy
r-muhairi (Feb 19 2023 at 14:57):Ali Caglayan said:
And if we are only building the stdlib for getting a working coq-core I believe there are some smarter things we can do.
right now, we're only getting coq-core it builds fine however on usage we need to be able to make the current env find the COQLIB if the stdlib is installed without having to explicitly specify an env
r-muhairi (Feb 19 2023 at 14:58):if coqc can detect it then coq-lsp should too
Ali Caglayan (Feb 19 2023 at 14:58):We can just set the COQLIB env var no?
r-muhairi (Feb 19 2023 at 14:58):Ali Caglayan said:
One thing I am trying to understand is that if a user has Coq available via Nix, are we able to plug the sources into the flake?
no that's another problem with having our own derivations for coq, they'll have to create their own
r-muhairi (Feb 19 2023 at 14:59):because nixpkgs doesn't even have 8.18+alpha yet
Ali Caglayan (Feb 19 2023 at 15:00):Would this be easier if Coq itself had a flake?
Ali Caglayan (Feb 19 2023 at 15:00):Then if Nixpkgs is just pinning a version of the Coq flake, we can easily compose
r-muhairi (Feb 19 2023 at 15:00):Ali Caglayan said:
Would this be easier if Coq itself had a flake?
channels or flakes is fine not sure if what they have currently builds, however we need the components to be split
Ali Caglayan (Feb 19 2023 at 15:01):Right we should open an issue in the Coq repo about that then
r-muhairi (Feb 19 2023 at 15:01):Ali Caglayan said:
We can just set the COQLIB env var no?
coq-lsp doesn't infer that now
r-muhairi (Feb 19 2023 at 15:02):you have to be explicit with --coqlib
r-muhairi (Feb 19 2023 at 15:02):it's better to just figure out how to actually have coqc detect coqlib if coq-stdlib is installed but im trying to figure out how
r-muhairi (Feb 19 2023 at 15:08):thing is @Ali Caglayan it's building coq-core with the path to coqlib already set in the config, but if coq-stdlib depends on coq-core we can't actually know the out path pre-eval
Ali Caglayan (Feb 19 2023 at 15:11):btw COQLIB isn't the path to the coq-stdlib, rather $COQLIB/theories is.
r-muhairi (Feb 19 2023 at 15:13):Ali Caglayan said:
btw COQLIB isn't the path to the coq-stdlib, rather
$COQLIB/theoriesis.
oh? That is in the outpath of coq-stdlib
Ali Caglayan (Feb 19 2023 at 15:13):To be clear coq-stdlib is a package so I guess having it one level up doesn't matter
r-muhairi (Feb 19 2023 at 15:15):Ali Caglayan said:
To be clear coq-stdlib is a package so I guess having it one level up doesn't matter
Ali Caglayan (Feb 19 2023 at 15:17):Yeah so coq-stdlib doesn't even contain anything
Ali Caglayan (Feb 19 2023 at 15:17):in the opam installation
Ali Caglayan (Feb 19 2023 at 15:17):It's all innstalled into a common coq directory.
Ali Caglayan (Feb 19 2023 at 15:17):coq-core and coq-stdlib
Ali Caglayan (Feb 19 2023 at 15:17):That common coq dir is COQLIB
r-muhairi (Feb 19 2023 at 15:18):can't we just use ocamlfind, surely the opam installation also exposes it through findlib no? but isn't used
Ali Caglayan (Feb 19 2023 at 15:19):I suppose so
Ali Caglayan (Feb 19 2023 at 15:19):tbh I have no idea anymore, sometimes I think I understand the install structure of Coq and then I get confused and realise I don't
Ali Caglayan (Feb 19 2023 at 15:19)::shrug:
r-muhairi (Feb 19 2023 at 15:19):@Emilio Jesús Gallego Arias
r-muhairi (Feb 19 2023 at 15:20):Ali Caglayan said:
tbh I have no idea anymore, sometimes I think I understand the install structure of Coq and then I get confused and realise I don't
my brain had enough of this for a day i'll push up the wrapped and uses env version
edit:
https://github.com/r-muhairi/coq-lsp/tree/ps/rr/_nix__build_without_submodules
Emilio Jesús Gallego Arias (Feb 19 2023 at 15:59):Hi folks, Indeed I think there are two separate topics here:
Emilio Jesús Gallego Arias (Feb 19 2023 at 15:59):We can add COQLIB and COQCORELIB to coq-lsp very trivially if we wish so
Emilio Jesús Gallego Arias (Feb 19 2023 at 16:00):I was just hoping to remove the duplication of that code with upstream, but that requires cycles I don't have given the other toplevels
Emilio Jesús Gallego Arias (Feb 19 2023 at 16:00):As you see Coq upstream uses a very simple method to infer COQCORELIB
Emilio Jesús Gallego Arias (Feb 19 2023 at 16:01):if the env var exists, use it, otherwise, use COQLIB/../coq-core
Ali Caglayan (Feb 19 2023 at 16:14):The problem is that when nix is building the derivation for coq-core it needs to know coqlib which will be used for theories detection later. However it cannot know that until coqlib is built, which can be a separate dir.
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:05):I see
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:06):You mean that the directory for coq-stdlib contains a hash?
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:06):that can't be predicted?
Ali Caglayan (Feb 19 2023 at 20:15):Right but that hash depends on building the stdlib with coqc configured with coqlib which gives us a circular dep
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:18):Mmmm
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:18):so where do Nix likes to puts these kind of config files
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:18):the config is in an ml file, but it doesn't have to be
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:19):using the env vars would be fine, we can add that easily
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:19):in fact let's do it
Ali Caglayan (Feb 19 2023 at 20:19):But the issue isn't for coq-lsp
Ali Caglayan (Feb 19 2023 at 20:19):Its for a separate derivatoin of coq-core and coq-stdlib
Ali Caglayan (Feb 19 2023 at 20:20):That doesn't seem to be possible
Ali Caglayan (Feb 19 2023 at 20:20):Not to mention, we currently are not able to share with the existing coq derivations because they are not granuar enough
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:25):coqcoqlib should disappear upstream, and except for some special cases, should be found using findlib
Emilio Jesús Gallego Arias (Feb 19 2023 at 20:25):but that has to happen usptream first
r-muhairi (Feb 19 2023 at 21:29):Emilio Jesús Gallego Arias said:
coqcoqlib should disappear upstream, and except for some special cases, should be found using findlib
Can't we use findlib for the coqlib as well?
Emilio Jesús Gallego Arias (Feb 19 2023 at 21:55):Maybe we could
Emilio Jesús Gallego Arias (Feb 19 2023 at 21:55):findlib is targetted to ocaml programs mostly tho
Emilio Jesús Gallego Arias (Feb 19 2023 at 21:55):so we are unsure about that
Emilio Jesús Gallego Arias (Feb 19 2023 at 21:56):but hopefully we use some standard mechanism, feedback from Nix is most appreciated actually
r-muhairi (Feb 19 2023 at 22:10):When installed with opam coq-stdlib is also exposed to findlib, I don't see why not if that's the current setup
r-muhairi (Feb 19 2023 at 22:11):Better than setting an env variable that's for sure especially in cases like coq-lsp whom don't fallback to the envvars I'd assume is quite often
r-muhairi (Feb 19 2023 at 22:12):We can expect lib/coq to be there then just fine
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:19):That's indeed interesting. However I think findlib is also setup in Nix in an env var :)
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:19):That's indeed interesting. However I think findlib is also setup in Nix in an env var :)
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:19):But yes that's an intersting idea to do in Coq
r-muhairi (Feb 19 2023 at 22:36):It's fine to just expose COQLIB as an env var for coq-stdlib I guess
r-muhairi (Feb 19 2023 at 22:37):To be honest, I see the point that Can't really justify using findlib that much after all it's just an empty/placeholder package
r-muhairi (Feb 19 2023 at 22:37):However it'll probably require some patches in some areas which I guess is to be expected
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:43):How do other languages like for example python solve this problem?
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:43):COQLIB in a sense is going away, we hope that soon all coq libs will be equal
Emilio Jesús Gallego Arias (Feb 19 2023 at 22:43):but still we need for the build system to understand where they are
r-muhairi (Feb 20 2023 at 12:19):Emilio Jesús Gallego Arias said:
How do other languages like for example python solve this problem?
are we talking on the nix side or?
Emilio Jesús Gallego Arias (Feb 20 2023 at 12:56):Yes @r-muhairi , on the nix side
Emilio Jesús Gallego Arias (Feb 20 2023 at 12:56):I understand that the python interpreter needs like a list of paths of where things are installed?
r-muhairi (Feb 21 2023 at 03:23):Two ways, either with buildEnv (done with withPackages) or explicitly set in PYTHONPATH
r-muhairi (Feb 21 2023 at 03:25): Emilio Jesús Gallego Arias (Feb 21 2023 at 03:55):Aha! Both ways should work for Coq, so that's up to you folks which one you prefer
Emilio Jesús Gallego Arias (Feb 21 2023 at 03:55):Thanks for the reference
r-muhairi (Feb 21 2023 at 06:58):@Ali Caglayan coq-lsp builds just fine without submodules now, however effectively packaging coq so we can actually use coq-lsp in nix environments is another problem. We can't be expected to distribute coq derivations from the coq-lsp flake.
Though that same problem does also apply for getting to test coq-lsp in the first place with nix environments
solved by a mere hack temporarily wrapping coq-lsp
Last updated: Apr 20 2024 at 13:01 UTC