Stream: Coq users

Topic: `Print` in `Coq.Init.Logic` behaves strangely


view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:08):

I was playing around with print statements inside foundational files, specifically Coq.Init.Logic, and I noticed that you can print a constant before it is defined:

Print not.
(* not = fun A : Prop => A -> Init.Logic.False
: Prop -> Prop *)
Definition not (A:Prop) := A -> False.
Definition not (A:Prop) := A -> False.
Print not.
(* not = fun A : Prop => A -> False
: Prop -> Prop *)

If I make a change to the definition it has effect only after the declaration (as I would expect), but it seems to be shadowing an import of itself?

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:09):

I observed this behavior in both CoqLSP and VsCoq 2

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:11):

this seems to be connected to the fact that there is no analogue of prelude at the top of the file indicating that one should not import the default imports

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:14):

I guess that Coq loads the prelude, so your first "not" refers to the compiled Init/Logic.vo file.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:15):

I agree, but that seems... bad? It's not supposed to be a dependency of itself

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:16):

you may pass the -no-init option to the compiler if you work on these files then.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:17):

ah, so it's an external thing?

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:17):

By default, Coq loads the prelude (Init).

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:18):

my point of reference here is lean, where you use import Foo at the top of the file to import module Foo and prelude to suppress the otherwise implicit import Init

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:19):

So here the equivalent of prelude would be this -no-init option.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:20):

so, basically the same as the -no-init flag but it's in the file itself, meaning that it will be processed the same way regardless of whether you get to it from an editor or coqc

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:21):

I don't think something like that exists in Coq. If it's a project-wise setting it can be set in the _CoqProject file.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:25):

hm, it appears that Init/_CoqProject exists and contains -arg -noinit, so I guess this is an issue in CoqLSP and VsCoq then since they aren't honoring this

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 13:30):

I don't know how they are supposed to work with _CoqProject files, sorry.

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 13:35):

proof general and coqide respect the _coqproject

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:37):

do you know which _CoqProject file applies to a given .v file? I notice that there is also a _CoqProject at the root of coq/theories, which does not have -noinit

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:38):

do they all apply or is it nearest-shadowing rules or something?

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 13:39):

the closest one should apply

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 13:49):

vscoq and coq-lsp may be detecting by looking from the top instead so they get the farther _coqproject

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 13:50):

if you delete the toplevel coqproject and reload do you still get the same results in Init/?

view this post on Zulip Mario Carneiro (Dec 20 2023 at 13:52):

yes, deletion or mangling of either file seems to make no difference so I guess it's not reading them at all?

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 13:53):

cc @Emilio Jesús Gallego Arias @Romain Tetley I guess

view this post on Zulip Pierre Rousselin (Dec 20 2023 at 14:01):

just tested with vim-coqtail, _CoqProject is taken into account.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:17):

@Mario Carneiro , indeed, Coq does From Coq Require Import Prelude. implictly, unless you pass -noinit. We tried to make this mandatory, but compat changes were too much.

What is likely happening with coq-lsp is that the workspace is set to theories, so it picks the _CoqProject file in theories; we assume projects have only one _CoqProject file, maybe it would be good to drop this restriction.

You can try instead opening the theories/Init folder. That "works for me" (TM)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:17):

[I mean using Open Folder in VSCode File menu]

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:25):

[The problem is that conceptually, for both Dune and coq-lsp, each _CoqProject defines a library, and all settings apply recursively, the easiest way to adapt coq stdlib to this model would be to put the prelude on its own dir, but maybe we manage to improve Dune's/coq-lsp to support this]

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:26):

Emilio Jesús Gallego Arias said:

Mario Carneiro , indeed, Coq does From Coq Require Import Prelude. implictly, unless you pass -noinit. We tried to make this mandatory, but compat changes were too much.

You mean to remove the concept of a prelude entirely?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:27):

@Gaëtan Gilbert analysis is spot-on, except for the bit about deleting _CoqProject in theories, in this case, coq-lsp will look at theories, and consider the project has no _CoqProject, as it only looks at the root of the workspace

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:27):

Mario Carneiro said:

Emilio Jesús Gallego Arias said:

Mario Carneiro , indeed, Coq does From Coq Require Import Prelude. implictly, unless you pass -noinit. We tried to make this mandatory, but compat changes were too much.

You mean to remove the concept of a prelude entirely?

Yes.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:27):

For example HoTT library does that, using -noinit

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:27):

I mean, having an implicit prelude is convenient for users, I'm not sure it would be a good default to start from scratch

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:28):

IMO the lean-style prelude keyword is a nice compromise: the imports are still explicitly encoded in the file but people don't have to worry about the horror that is writing code without any library

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:29):

Indeed, but on the other hand we need to handle the prelude specially, which is a nuisance in other contexts (for example Dune has to insert the Init/Prelude.vo dependency after analysis of the command line flags

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:29):

I agree that it is weird to have exactly one of your many imports expressed via a side channel

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:30):

Thanks for the tip about Lean's behavior, I'll look into it!

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:31):

Emilio Jesús Gallego Arias said:

Gaëtan Gilbert analysis is spot-on, except for the bit about deleting _CoqProject in theories, in this case, coq-lsp will look at theories, and consider the project has no _CoqProject, as it only looks at the root of the workspace

Note that this was when I was browsing the coq repo itself, so the root is not theories but its parent

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:32):

As things stand now, if you set the coq sources as root, coq-lsp will determine there is no _CoqProject file.

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:32):

and there is indeed no _CoqProject at the coq project root (which seems ironic somehow)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:33):

Things do work tho as it will use the Prelude from the installed Coq

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:33):

yeah, I was surprised that coq is fine with this, lean would blow up if you imported a file in itself because of name collisions

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:33):

But indeed here you are facing a case we handle very poorly (or not all, it can be argued)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:34):

Mario Carneiro said:

yeah, I was surprised that coq is fine with this, lean would blow up if you imported a file in itself because of name collisions

Exactly. This is pretty bad.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:34):

Given a coq source tree, you need to compile with that precise coqc both coq-lsp and the coq libraries to ensure things are compatible. We don't have a stable good way to do this now (other than a make + install hell)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:35):

coq-universe does solve this, as you setup a full tree with all the deps, which are composed for build correctly.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:36):

But so far coq-universe is not yet ready for more general use, but indeed, it will solve most problems.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:36):

In the sense of these deps.

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 14:37):

Mario Carneiro said:

yeah, I was surprised that coq is fine with this, lean would blow up if you imported a file in itself because of name collisions

coq fails too, but with no _CoqProject detected the current file is called Logic but the auto imported file is called Coq.Init.Logic

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:39):

are there any other side effects of double defining a library, assuming the root module name is different but the text is the same? e.g. double defined syntax causing ambiguities

view this post on Zulip Gaëtan Gilbert (Dec 20 2023 at 14:39):

that is why you got

Print not.
(* not = fun A : Prop => A -> Init.Logic.False
: Prop -> Prop *)

presumably you did the Print between Inductive False and Definition not, so not refers to Coq.Init.Logic.not which is about Coq.Init.Logic.False and not the local Logic.False

view this post on Zulip Mario Carneiro (Dec 20 2023 at 14:41):

I guess any use of full names will resolve differently

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:41):

There is tho a way to explore the stdlib with coq-lsp for coq master that is not _too_ painful, checkout coq-lsp main branch, then do make submodules-init && make; then you can do dune exec -- code vendor/coq/theories (or vendor/coq/theories/Init and things "should work" (TM)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 20 2023 at 14:41):

[be sure that code is closed before doing the call tho, otherwise it won't be launched, but the existing instance will be run, with wrong PATH]

view this post on Zulip Pierre Roux (Dec 20 2023 at 15:27):

BTW, about the initial question, to known which not is which, one can About not. (or simply Locate not to get the fully qualified name Coq.Init.Logic.not


Last updated: Jun 13 2024 at 19:02 UTC