Stream: Dune devs & users

Topic: dune and coqc -R vs -Q


view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 01:55):

https://coq.inria.fr/refman/practical-tools/utilities.html?highlight=dune#building-a-coq-project-with-dune suggests (in an example) that dune uses the -R flag (in (name Equations) ; -R flag), and I've seen that myself at some point. However, what I want dune to use is (obviously?) -Q. What does dune actually do?

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 02:00):

Just tried again and dune uses -R — even tho I passed (include_subdirs qualified) — which seems to imply -Q.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 02:01):

~meanwhile the dune manual claims that include_subdirs only supports no and unqualified (https://dune.readthedocs.io/en/stable/dune-files.html#include-subdirs)~ ah, the mistake is quickly explained: that section is only about OCaml code.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 02:03):

https://dune.readthedocs.io/en/stable/dune-files.html#recursive-qualification-of-modules mentions (include_subdirs qualified), but the other section doesn't account for it.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 02:05):

more annoying, dune's "declarative builds" sometimes feel like "dune knows better than you", which is nice until it isn't :-| — I'm not sure how to make this constructive, except that e.g. sbt was much more extensible in this regard.

view this post on Zulip Li-yao (Nov 29 2020 at 18:03):

Relevant ticket: https://github.com/ocaml/dune/issues/2585

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 18:12):

We already have an issue open to make include_subdirs per-language, that should help

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 18:13):

Regarding -Q vs -R , we used -R for the local library as this is what OCaml does, and imagine you refactor and change the name, that's a pain, for external ones, -Q is always used. But indeed -Q vs -R is a low-level detail, that should hopefully go away and replaced by a higher level theory setup

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 18:15):

https://github.com/ocaml/dune/issues/3314

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 19:59):

I’m afraid I don’t follow. I want -Q for the local library, and I didn’t think that was controversial; it sounds like you disagree?

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 19:59):

Either way, I’m not convinced it’s dune’s business to choose for me...

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 20:09):

Thinking again, your argument for -R is interesting, but I’m not sure if it actually works. For it to help, I’d need to actually take advantage of -R, so it’d have to be documented.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 20:11):

But am I going mad or -R should translate to include_subdirs unqualified while -Q should translate to include_subdirs qualified?

view this post on Zulip Rudi Grinberg (Nov 29 2020 at 22:30):

@Paolo Giarrusso In the OCaml world, (include_subdirs qualified) seems to be strictly superior to (include_subdirs unqualified). Once we introduce (include_subdirs qualified), we'll essentially softly deprecate the old mode. I don't know enough about coq, but why would you ever want the unqualified version?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 22:36):

@Paolo Giarrusso indeed unqualified doesn't do what you think, it merges everything in flat mode and indeed it may be removed. In Coq think of just recursive or not recursive. -R is an implementation detail, the point is that if you want to do, for a library Foo:

Require Import Foo.A

or just Require Import A in the files of the same library. Second form has some advantages, for example if you rename your library to Bar, nothing has to change; it also helps with vendoring as you can properly create unique names.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 22:57):

I’m still unsure how Dune works here, and I’m not talking about the implementation detail, I’m disagreeing on the substance. It should be clear whether Require Import A. works or not, and I don’t think it should.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 22:59):

Today I have a choice, and I (or rather, I and my team) choose to use -Q uniformly, because I don’t want code changing behavior between different libraries I co-maintain.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:00):

@Rudi Grinberg I don’t understand what you mean by “qualified” and “unqualified” — that’s part of the question. I’m also not an OCaml programmer, and I’m not alone.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:02):

I’m also confused by “recursive or not recursive”.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:02):

Yeah, forget about unqualified, it has some hacky semantics, basically joining all modules under a flat include space. For Coq it is either recursive or not, where recursive mean, consider all subdirs, whereas non-recursive means, consider only the current dir.

So the current intended semantics are: imagine you have a lib src/A.v src/B.v, with (name Foo)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):

also src/bar/C.v

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):

So for example, from module src/B.v

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:03):

confused, but I think I understand -R and -Q

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):

you can do Require Import A and Require Import bar.C

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):

however, if you are using Foo from another theory

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):

then you must use From Foo Require Import A , etc...

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:04):

Exactly

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):

Yeah that's the convention in OCaml as it tends to be a bit more convenient

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):

What is frowned upon generally

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):

is adding external libraries with -R semantics

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):

for the local ones, I guess it is OK

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):

you could also use -Q for them but seems a bit annoying

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:05):

this is the first I hear of this convention

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):

Well, Coq has no notion of library at all

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):

in the first place, the notion of theory was introduced by Dune so indeed we did some choices

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:06):

Coq works by dumping all files toghether

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:06):

not the nicest way

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:06):

my way of using Coq is never using -R.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:06):

so both models are possible, for now we choose this one [as done in OCaml]

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):

my way of using Coq is never using -R

Yup that's not a bad default when you lack a notion of library

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):

once you can distinguish betwwen compilation units

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):

other options are possible

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):

it is normal for coq_makefile users to default to -Q as everything is merged up together

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:08):

but it seems other options are possible today

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):

actually using -R in Coq makefile indeed it seems like a bad idea

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:08):

hm, not sure — couldn’t you use -R locally and install them otherwise?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):

Yes, it works

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):

loadpath code in Coq is ... interesting

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:09):

we don't even know if it works by chance or not

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:09):

[we => I don't even know]

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:09):

still

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:09):

the fact that there are 3 copies of it doesn't help [one for coqchk, one for coqdep, one for coqdoc, and one for coqc/coqtop]

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:10):

I think I’d still prefer a choice.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:10):

I don’t like paternalism from a build tool.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:10):

Especially behind my back, even tho I don’t think it was intentional.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:11):

Umm, I guess you are thinking a bit low-level here, but indeed, there is a tradeoff

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:11):

I would not say "paternalism", but tooling is inherentily opinionated

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:11):

not really, -R and -Q are the “high-level” view to me, that’s all I know

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:11):

adding too many options, it becomes a hell to maintain test

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:12):

These are extremely low-level to me, they are talking about the filesystem

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:12):

as a rule, dune-speak means little to me

view this post on Zulip Rudi Grinberg (Nov 29 2020 at 23:12):

Paolo Giarrusso said:

I think I’d still prefer a choice.

Curious if Scala allows such a choice. I don't of many languages that don't force a file system layout on you. C, Ruby come to mind. Not very good company :)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:13):

@Paolo Giarrusso you speak low-level, that is fine, however that low-level prevents from having a lot of features that people would find interesting

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:13):

such as proper interfaces / implementations, of versioned linking, notions of virtual packages or even namespaces

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:13):

s/low-level/the only interface I know: the coq_makefile one/

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):

so IMHO we have to move to a view that is more focused on use cases and not on low-level flags

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):

I mean, coq-makefile in itself is not even a tool

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):

it is just a template

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):

a makefile template

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):

which some program that just substitues some config-time variables

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:14):

are you familiar with the “curse of knowledge”?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:15):

as such, it is extremely primitive

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:15):

Yes I am

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:15):

good.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:16):

As a first approximation, the entirety of dune-speak suffers from that.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):

you would expect me to be familiar with it

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):

what is dune-speak

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:16):

I’m only checking because it seems very much in play

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):

I am trying to talk about more general concepts

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):

for example, what is a library

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):

what it means to depend on another library / theory?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):

the reason these notions are linked to dune is just because Dune is the first system to implement them for Coq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):

but in no way are specific, and indeed make-based people could chose to implement a similar model

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:17):

I’m not sure I agree.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):

well, for example

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):

whether from a theory Foo , I want to do From Foo Require A or just Require A

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):

that seems to me pretty much independent of dune

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):

actually dune doesn't care at all , a 10 line patch would add the corresponding config option

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:18):

indeed, except that dune has its opinions :-)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):

any piece of code has an opinion of course

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):

I don't see that as a bad thing

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:18):

unclear, some code is more opinionated.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):

design by comittee worries me much more

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:19):

in this case dune doesn't have an opinion on that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:19):

as it has little impact [5-10 lines of code]

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:19):

today, in practice, it does.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:19):

but it keeps it to itself.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:20):

not sure I follow, anyways, got to go, see you tomorrow?

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:20):

absolutely don’t let me keep you, can I reply asynchronously?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:20):

Sure

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:22):

TLDR: without clear docs, a user can’t even decide to take advantage of this behavior. At best, they’ll get confusing results if they user Require Import A by mistake — but never seen that in practice. (Possibly, we suffer the warnings from it — if it’s true that the warnings from coqdep on duplicate modules are -R-specific).

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:25):

The problem with the warnings is very different and happens under -Q

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):

But I insist that Dune has no opinion on that yet

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:26):

@Rudi Grinberg my question is not really about filesystem layout, but about Require behavior. In Java/Scala, the question doesn’t arise because the build tool can’t ever affect what imports are valid; the fully qualified name of a class can be deduced by its source file.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):

It is implementing a version that imitates the OCaml smenatics

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):

but the reason the issue you have just seen is still open

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):

is that still is not clear what the opinion on that is

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):

the issue is open well, because we recognize is an issue

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

however the solution is not simple due to other features, composition etc...

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

if dune had an opinion o that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

on that, I'd close the issue as wontfix

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

however the answer is neither 'let's use -Q`

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

as that may brings some other problems

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:27):

to be sure, we use “have an opinion” for different things

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):

so that's why I'm asking, for high-level use cases and preference

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:28):

ah

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28):

a bug is not an opinion

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28):

:)

view this post on Zulip Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28):

what you point out is, as of today, an unresolved bug

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:28):

whatever the intention, dune gives me -R, that’s all

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:28):

at a high-level

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:29):

I don’t want to alter my imports because I move my code across libraries.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:29):

I work on a “virtual monorepo” split into different repos

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:31):

and I prefer the meaning to be as close as possible across different files (within reason). If it isn’t, I need to know, and document that internally as a foot-gun.

view this post on Zulip Paolo Giarrusso (Nov 29 2020 at 23:34):

or maybe change my mental model so that this behavior is natural, but I need to know.

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 20:32):

Updates: even when using and exploiting -R foo, it's tricky to make the code agnostic to its logical-path prefix — foo must still be used with From

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 20:43):

which seems also the case with Coq, e.g. From Lists Import List. doesn't let you import Coq.Lists.List.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:00):

You mean with -Q ? Not sure what you wanna say above, indeed From refers to the root , so it has to be From Coq Require Import blah

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:03):

I do mean with -R

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:05):

I have (coq.theory (name brauto.tests)), but I was trying to never mention brauto.tests in source — this code is not supposed to be usable by clients, and that prefix used to be empty.

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:07):

then I tried to refactor Require long_foo.a long_foo.b long_foo.c to From long_foo Require a b c, but that doesn't work

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):

yeah, that doesn't work

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):

but it is a good idea if it worked indeed

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):

rules for qualified names are a different indeed in Coq

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:09):

so maybe your -open proposal should make that work?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:09):

indeed you convinced me to implement a flag that will do what you here and in other exapmles

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:09):

exactly

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:09):

Thanks for the feedback as indeed it is important to design this stuff well

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:09):

that's why I didn't want to rush with the "1.0" build language

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:09):

I'm uncertain myself, and this might warrant a CEP

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):

I have a PR incoming so we may discuss a bit there

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):

A CEP could work, but IMHO it is going to be best to implement something and have people try it

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):

gather feedback, refine

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):

and declare it stable when we are happy

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:11):

CEPs may not do the best job anticipating all use cases here IMO

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2020 at 22:11):

and compatibility issues!

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:11):

FWIW, the use case here was that the prefix used to be empty (this is test code), and -Q path "" doesn't exist...

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:11):

fair point

view this post on Zulip Paolo Giarrusso (Dec 13 2020 at 22:12):

indeed, IETF drafts must be implemented before standardization


Last updated: Oct 16 2021 at 07:02 UTC