Stream: Coq users

Topic: ✔ Find location of imported file


view this post on Zulip Julin Shaji (Feb 15 2024 at 16:11):

From within a coq file, is there a way to the file location of another coq file that we have imported into the current file?

For example, suppose we have two coq files Another.v and Current.v.
In Current.v, I do Require Import Another..
Afterwards, is there a vernacular command to figure out the location of Another.v?

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:12):

For a situation where Coq has no errors, but the user has no idea of the location of the file.

view this post on Zulip Guillaume Melquiond (Feb 15 2024 at 16:13):

Locate Module Another.

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:14):

I was looking for the path to a file. As in /home/user/repos/my-library/theories/Another.v. Is that possible?

view this post on Zulip Guillaume Melquiond (Feb 15 2024 at 16:15):

Not directly, I think. You can combine Locate Module with Print LoadPath to recover the full path.

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:15):

Ah.. I guess it's Locate Library Another. Thanks!

view this post on Zulip Guillaume Melquiond (Feb 15 2024 at 16:16):

Oh. Didn't know about this one.

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:17):

It gives location of the compiled .vo file. Not the .v file. But that's what I wanted. :-)

view this post on Zulip Notification Bot (Feb 15 2024 at 16:20):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2024 at 16:35):

@Julin Shaji , indeed locating the .v file directly is not possible from coqc / coqtop, you can only locate the .vo file.

The build system knows where the .v files are.

In most cases, .vo files will be next to their corresponding .v files, however there are exceptions I'm afraid.

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:54):

I was looking for such an option to figure out a build error.

I was trying to build this library: https://github.com/coq-community/reglang (v1.2.1)

I compiled mathcomp2 from its repo (v2.2.0).
Then I appended this to the _CoqProject file:

-I /home/user/repos/math-comp/mathcomp
-R /home/user/repos/math-comp/mathcomp mathcomp

-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden
-arg -w -arg +duplicate-clear
-arg -w -arg +non-primitive-record
-arg -w -arg +undeclared-scope
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar

When I use make to build reglang, it works fine.

But when I use dune build, it gives error:

Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune
3.8 and will be removed in an upcoming Dune version.
File "./theories/misc.v", line 99, characters 52-57:
Error:
In environment
T : finType
p : pred T
eq_pT : #|{: {x : T | p x}}| = #|T|
The term "{x : T | p x}" has type "Type" while it is expected to have type
 "finType".

Yet misc.v has no error when I step through it in the text editor.

So I tried putting Locate Library all_ssreflect. inside misc.v like:

(* Authors: Christian Doczkal and Jan-Oliver Kaiser *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import all_ssreflect.

Locate Library all_ssreflect.

When I step through it in editor, Locate is showing the correct
path: /home/user/repos/math-comp/mathcomp/ssreflect/all_ssreflect.vo

But when I do it with dune build, it is giving error:

File "./theories/misc.v", line 5, characters 0-29:
Error: Cannot find a physical path bound to logical path all_ssreflect.

Funnily enough there was no error when all_ssreflect was imported.

I guess this has to do with something related to _CoqProject. But I
am yet to figure out why..

view this post on Zulip Gaëtan Gilbert (Feb 15 2024 at 16:57):

dune doesn't look at _coqproject

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:57):

Duh.. I think I now know part of the reason for this error.
I already had another mathcomp version in path.

But I've now removed it.

view this post on Zulip Julin Shaji (Feb 15 2024 at 16:58):

Gaëtan Gilbert said:

dune doesn't look at _coqproject

So I need to look for a way to make dune use the mathcomp that I've compiled from the repo source?

How can I do that?

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:12):

Then I guess what I'm looking for is a way to use a library built with make as a dependency for a library being built with dune. Is that possible?

view this post on Zulip Pierre Roux (Feb 15 2024 at 17:24):

I'm not sure why you don't just install mathcomp (either from source or using Opam, Nix, whatever package manager you used to install Coq itself).

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:30):

I wanted mathcomp2. I used to use mathcomp from nix. But it's still on v1.18

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:31):

And coq is from nix. If opam is to be used, I would have to have another copy of coq as well, right? That's why I tried compiling from source.

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:34):

I guess one way would be write a nix derivation for mathcomp2. But I just use nix for the stuff that's already there and still don't know to make a custom nix derivation.

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:35):

Oh, just saw that you meant installing it.

view this post on Zulip Julin Shaji (Feb 15 2024 at 17:36):

I didn't want to make it permanent. I wanted the flexibility to use another version if needed. Like mathcomp1 for example.

view this post on Zulip Pierre Roux (Feb 15 2024 at 17:41):

There is already a mathcomp 2 derivation in nixpkgs but I must admit I don't know how to use it outside the coq-nix-toolbox (or more precisely I never remember the cryptic syntax). I'd love to make mathcomp2 the default in nixpkgs but I guess we still have to wait for a few last things to switch. @Vincent Laporte would probably have a more informed opinion.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2024 at 19:31):

Julin Shaji said:

Gaëtan Gilbert said:

dune doesn't look at _coqproject

So I need to look for a way to make dune use the mathcomp that I've compiled from the repo source?

How can I do that?

I think COQPATH should work and is the preferred method for Nix, no?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2024 at 19:32):

That project is using 0.3 dune build lang, so in this case, Dune doesn't mess with deps a lot

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2024 at 19:33):

As you can see in _build/log it will just call coqc and let coqc figure out where the stuff is in a standard way

view this post on Zulip Emilio Jesús Gallego Arias (Feb 15 2024 at 19:33):

Starting with Coq dune build language 0.8, Dune indeed will use instead coqc -boot, so it hides stuff in the default COQPATH + user-contrib, unless the user declares the dep

view this post on Zulip Vincent Laporte (Feb 15 2024 at 20:05):

Julin Shaji said:

I wanted mathcomp2. I used to use mathcomp from nix. But it's still on v1.18

Mathcomp 2 is available in nixpkgs, but indeed, it is not the default version. You may have to override the mathcomp package in order to get it (as in mathcomp.override { version = "2.1.0"; }). Here is a complete (minimal?) example: put the following in a file and call nix-shell with the file name as argument:

with import <nixpkgs> {};

mkShell {

  packages = with coqPackages; [
    coq
    (mathcomp.override { version = "2.1.0"; })
  ];

}

view this post on Zulip Julin Shaji (Feb 16 2024 at 07:25):

Thanks, that nix file made the compilation work for reglang.

view this post on Zulip Julin Shaji (Feb 16 2024 at 07:30):

Vincent Laporte said:

Julin Shaji said:

I wanted mathcomp2. I used to use mathcomp from nix. But it's still on v1.18

Mathcomp 2 is available in nixpkgs, but indeed, it is not the default version. You may have to override the mathcomp package in order to get it (as in mathcomp.override { version = "2.1.0"; }). Here is a complete (minimal?) example: put the following in a file and call nix-shell with the file name as argument:

with import <nixpkgs> {};

mkShell {

  packages = with coqPackages; [
    coq
    (mathcomp.override { version = "2.1.0"; })
  ];

}

How can one know whether a new version of a package is available in nixpkgs?

I was wondering if the new version of reglang itself can be obtained from nix. Its nix file seems to mention reglang v1.2.0 in nixpkgs v23.11 (and reglang v1.2.1 in master): https://github.com/NixOS/nixpkgs/blob/nixpkgs-23.11-darwin/pkgs/development/coq-modules/reglang/default.nix
Can that be used?

I tried:

with import <nixpkgs> {};

mkShell {

  packages = (with coqPackages; [
    coq
    (mathcomp.override { version = "2.1.0"; })
    (reglang.override { version = "1.2.0"; })
  ]) ++ [
    dune_3
    opam
    ocaml
    emacs
  ];
}

but that gave error:

this derivation will be built:
  /nix/store/vrbfvbp1pgawl6gkybhazifp0gy1hqx0-coq8.18-reglang-1.2.0.drv
warning: Ignoring setting 'auto-allocate-uids' because experimental feature 'auto-allocate-uids' is not enabled
warning: Ignoring setting 'impure-env' because experimental feature 'configurable-impure-env' is not enabled
building '/nix/store/vrbfvbp1pgawl6gkybhazifp0gy1hqx0-coq8.18-reglang-1.2.0.drv'...
Running phase: unpackPhase
unpacking source archive /nix/store/jgn0mlip08gxcr6cmr3v92x5axmipq2y-source
source root is source
Running phase: patchPhase
Running phase: updateAutotoolsGnuConfigScriptsPhase
Running phase: configurePhase
no configure script, doing nothing
Running phase: buildPhase
build flags: -j16 SHELL=/nix/store/7dpxg7ki7g8ynkdwcqf493p2x8divb4i-bash-5.2-p15/bin/bash
/nix/store/minbk2amvx7s5ynvmknzb4564aa75q62-coq-8.18.0/bin/coq_makefile -f _CoqProject -o Makefile.coq
make[1]: Entering directory '/build/source'
COQDEP VFILES
*** Warning: in file theories/languages.v, library structures is required from root HB and has not been found in the loadpath!
*** Warning: in file theories/regexp.v, library structures is required from root HB and has not been found in the loadpath!
*** Warning: in file theories/minimization.v, library structures is required from root HB and has not been found in the loadpath!
COQC theories/misc.v
COQC theories/setoid_leq.v
File "./theories/misc.v", line 99, characters 52-57:
Error:
In environment
T : finType
p : pred T
eq_pT : #|{: {x : T | p x}}| = #|T|
The term "{x : T | p x}" has type "Type" while it is expected to have type
 "finType".

make[2]: *** [Makefile.coq:838: theories/misc.vo] Error 1
make[2]: *** [theories/misc.vo] Deleting file 'theories/misc.glob'
make[2]: *** Waiting for unfinished jobs....
make[1]: *** [Makefile.coq:409: all] Error 2
make[1]: Leaving directory '/build/source'
make: *** [Makefile:2: all] Error 2
error: builder for '/nix/store/vrbfvbp1pgawl6gkybhazifp0gy1hqx0-coq8.18-reglang-1.2.0.drv' failed with exit code 2

No error is there if the line about reglang is commented. Maybe reglang v1.2.0 is not there in nixpkgs yet?

view this post on Zulip Vincent Laporte (Feb 16 2024 at 07:33):

I guess that this version of reglang requires mathcomp 2, so a simple override will not work.

view this post on Zulip Julin Shaji (Feb 16 2024 at 07:34):

Yes it needs mathcomp2. I guess it's more complicated then?

view this post on Zulip Vincent Laporte (Feb 16 2024 at 07:35):

Yes, you’ll have to override mathcomp in the whole coqPackages set.

view this post on Zulip Julin Shaji (Feb 16 2024 at 07:39):

Can we mention version in a coqPackages.override? I was looking at https://nixos.org/guides/nix-pills/nixpkgs-overriding-packages.html and they only seem to mention stuff like flags.

view this post on Zulip Vincent Laporte (Feb 16 2024 at 07:57):

Here you go:

with import <nixpkgs> {};


let cP = coqPackages.overrideScope' (self: super: {
  mathcomp = super.mathcomp.override { version = "2.1.0"; };
});
in

mkShell {

  packages = with cP; [
    coq
    reglang
  ];

}

view this post on Zulip Vincent Laporte (Feb 16 2024 at 08:01):

With overrideScope', you can build a consistent package set: all packages within the set will see the override. In this case, reglang will receive mathcomp 2 as input and default to version 1.2.

view this post on Zulip Julin Shaji (Feb 16 2024 at 08:10):

Thanks a lot! It worked.

view this post on Zulip Julin Shaji (Feb 16 2024 at 08:11):

How can we know if a particular version of a package has been put in nixpkgs or not? In the case of reglang, its default.nix file had some mention of the newer version. But for mathcomp, I couldn't find even that.

view this post on Zulip Vincent Laporte (Feb 16 2024 at 08:14):

Here are the versions of mathcomp that are known: https://github.com/NixOS/nixpkgs/blob/2c7c560330ee7b4089d27887f66ef0fe249bf866/pkgs/development/coq-modules/mathcomp/default.nix#L41-L58
I have to say that indeed this is not really convenient.

view this post on Zulip Julin Shaji (Feb 16 2024 at 08:14):

Oh.. had missed that. Thanks.

view this post on Zulip Vincent Laporte (Feb 16 2024 at 09:47):

For future reference: https://nixos.wiki/wiki/Coq#Using_non-default_versions_of_packaged_libraries

view this post on Zulip Notification Bot (Feb 23 2024 at 13:14):

14 messages were moved from this topic to #Nix toolbox devs & users > mathcomp2 via nix by Théo Zimmermann.


Last updated: Jun 22 2024 at 15:01 UTC