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?
Just tried again and dune uses
-R — even tho I passed
(include_subdirs qualified) — which seems to imply
~meanwhile the dune manual claims that
include_subdirs only supports
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.
(include_subdirs qualified), but the other section doesn't account for it.
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.
Relevant ticket: https://github.com/ocaml/dune/issues/2585
We already have an issue open to make
include_subdirs per-language, that should help
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
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?
Either way, I’m not convinced it’s dune’s business to choose for me...
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.
But am I going mad or
-R should translate to
include_subdirs unqualified while
-Q should translate to
@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?
@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
-R is an implementation detail, the point is that if you want to do, for a library
Require Import Foo.A
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.
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.
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.
@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.
I’m also confused by “
recursive or not
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
So for example, from module
confused, but I think I understand
you can do
Require Import A and
Require Import bar.C
however, if you are using
Foo from another theory
then you must use
From Foo Require Import A , etc...
Yeah that's the convention in OCaml as it tends to be a bit more convenient
What is frowned upon generally
is adding external libraries with
for the local ones, I guess it is OK
you could also use
-Q for them but seems a bit annoying
this is the first I hear of this convention
Well, Coq has no notion of library at all
in the first place, the notion of theory was introduced by Dune so indeed we did some choices
Coq works by dumping all files toghether
not the nicest way
my way of using Coq is never using
so both models are possible, for now we choose this one [as done in OCaml]
my way of using Coq is never using -R
Yup that's not a bad default when you lack a notion of library
once you can distinguish betwwen compilation units
other options are possible
it is normal for coq_makefile users to default to -Q as everything is merged up together
but it seems other options are possible today
-R in Coq makefile indeed it seems like a bad idea
hm, not sure — couldn’t you use
-R locally and install them otherwise?
Yes, it works
loadpath code in Coq is ... interesting
we don't even know if it works by chance or not
[we => I don't even know]
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]
I think I’d still prefer a choice.
I don’t like paternalism from a build tool.
Especially behind my back, even tho I don’t think it was intentional.
Umm, I guess you are thinking a bit low-level here, but indeed, there is a tradeoff
I would not say "paternalism", but tooling is inherentily opinionated
-Q are the “high-level” view to me, that’s all I know
adding too many options, it becomes a hell to maintain test
These are extremely low-level to me, they are talking about the filesystem
as a rule, dune-speak means little to me
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 :)
@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
such as proper interfaces / implementations, of versioned linking, notions of virtual packages or even namespaces
s/low-level/the only interface I know: the coq_makefile one/
so IMHO we have to move to a view that is more focused on use cases and not on low-level flags
I mean, coq-makefile in itself is not even a tool
it is just a template
a makefile template
which some program that just substitues some config-time variables
are you familiar with the “curse of knowledge”?
as such, it is extremely primitive
Yes I am
As a first approximation, the entirety of dune-speak suffers from that.
you would expect me to be familiar with it
what is dune-speak
I’m only checking because it seems very much in play
I am trying to talk about more general concepts
for example, what is a library
what it means to depend on another library / theory?
the reason these notions are linked to dune is just because Dune is the first system to implement them for Coq
but in no way are specific, and indeed make-based people could chose to implement a similar model
I’m not sure I agree.
well, for example
whether from a theory
Foo , I want to do
From Foo Require A or just
that seems to me pretty much independent of dune
actually dune doesn't care at all , a 10 line patch would add the corresponding config option
indeed, except that dune has its opinions :-)
any piece of code has an opinion of course
I don't see that as a bad thing
unclear, some code is more opinionated.
design by comittee worries me much more
in this case dune doesn't have an opinion on that
as it has little impact [5-10 lines of code]
today, in practice, it does.
but it keeps it to itself.
not sure I follow, anyways, got to go, see you tomorrow?
absolutely don’t let me keep you, can I reply asynchronously?
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
The problem with the warnings is very different and happens under -Q
But I insist that Dune has no opinion on that yet
@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.
It is implementing a version that imitates the OCaml smenatics
but the reason the issue you have just seen is still open
is that still is not clear what the opinion on that is
the issue is open well, because we recognize is an issue
however the solution is not simple due to other features, composition etc...
if dune had an opinion o that
on that, I'd close the issue as wontfix
however the answer is neither 'let's use -Q`
as that may brings some other problems
to be sure, we use “have an opinion” for different things
so that's why I'm asking, for high-level use cases and preference
a bug is not an opinion
what you point out is, as of today, an unresolved bug
whatever the intention, dune gives me
-R, that’s all
at a high-level
I don’t want to alter my imports because I move my code across libraries.
I work on a “virtual monorepo” split into different repos
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.
or maybe change my mental model so that this behavior is natural, but I need to know.
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
which seems also the case with Coq, e.g.
From Lists Import List. doesn't let you import
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
I do mean with
(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.
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
yeah, that doesn't work
but it is a good idea if it worked indeed
rules for qualified names are a different indeed in Coq
so maybe your
-open proposal should make that work?
indeed you convinced me to implement a flag that will do what you here and in other exapmles
Thanks for the feedback as indeed it is important to design this stuff well
that's why I didn't want to rush with the "1.0" build language
I'm uncertain myself, and this might warrant a CEP
I have a PR incoming so we may discuss a bit there
A CEP could work, but IMHO it is going to be best to implement something and have people try it
gather feedback, refine
and declare it stable when we are happy
CEPs may not do the best job anticipating all use cases here IMO
and compatibility issues!
FWIW, the use case here was that the prefix used to be empty (this is test code), and
-Q path "" doesn't exist...
indeed, IETF drafts must be implemented before standardization
Last updated: Jun 03 2023 at 17:29 UTC