Paolo Giarrusso (Nov 29 2020 at 01:55): 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?
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.
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.
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.
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.
Li-yao (Nov 29 2020 at 18:03):Relevant ticket: https://github.com/ocaml/dune/issues/2585
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
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 18:15):https://github.com/ocaml/dune/issues/3314
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?
Paolo Giarrusso (Nov 29 2020 at 19:59):Either way, I’m not convinced it’s dune’s business to choose for me...
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.
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?
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?
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.
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.
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.
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.
Paolo Giarrusso (Nov 29 2020 at 23:02):I’m also confused by “recursive or not recursive”.
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)
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):also src/bar/C.v
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):So for example, from module src/B.v
Paolo Giarrusso (Nov 29 2020 at 23:03):confused, but I think I understand -R and -Q
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):you can do Require Import A and Require Import bar.C
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:03):however, if you are using Foo from another theory
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):then you must use From Foo Require Import A , etc...
Paolo Giarrusso (Nov 29 2020 at 23:04):Exactly
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):What is frowned upon generally
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:04):is adding external libraries with -R semantics
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):for the local ones, I guess it is OK
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):you could also use -Q for them but seems a bit annoying
Paolo Giarrusso (Nov 29 2020 at 23:05):this is the first I hear of this convention
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:05):Well, Coq has no notion of library at all
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:06):Coq works by dumping all files toghether
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:06):not the nicest way
Paolo Giarrusso (Nov 29 2020 at 23:06):my way of using Coq is never using -R.
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]
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):once you can distinguish betwwen compilation units
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:07):other options are possible
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
Paolo Giarrusso (Nov 29 2020 at 23:08):but it seems other options are possible today
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):actually using -R in Coq makefile indeed it seems like a bad idea
Paolo Giarrusso (Nov 29 2020 at 23:08):hm, not sure — couldn’t you use -R locally and install them otherwise?
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):Yes, it works
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:08):loadpath code in Coq is ... interesting
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:09):we don't even know if it works by chance or not
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:09):[we => I don't even know]
Paolo Giarrusso (Nov 29 2020 at 23:09):still
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]
Paolo Giarrusso (Nov 29 2020 at 23:10):I think I’d still prefer a choice.
Paolo Giarrusso (Nov 29 2020 at 23:10):I don’t like paternalism from a build tool.
Paolo Giarrusso (Nov 29 2020 at 23:10):Especially behind my back, even tho I don’t think it was intentional.
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:11):I would not say "paternalism", but tooling is inherentily opinionated
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:11):adding too many options, it becomes a hell to maintain test
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:12):These are extremely low-level to me, they are talking about the filesystem
Paolo Giarrusso (Nov 29 2020 at 23:12):as a rule, dune-speak means little to me
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 :)
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
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
Paolo Giarrusso (Nov 29 2020 at 23:13):s/low-level/the only interface I know: the coq_makefile one/
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):I mean, coq-makefile in itself is not even a tool
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):it is just a template
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):a makefile template
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:14):which some program that just substitues some config-time variables
Paolo Giarrusso (Nov 29 2020 at 23:14):are you familiar with the “curse of knowledge”?
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:15):as such, it is extremely primitive
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:15):Yes I am
Paolo Giarrusso (Nov 29 2020 at 23:15):good.
Paolo Giarrusso (Nov 29 2020 at 23:16):As a first approximation, the entirety of dune-speak suffers from that.
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):you would expect me to be familiar with it
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):what is dune-speak
Paolo Giarrusso (Nov 29 2020 at 23:16):I’m only checking because it seems very much in play
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):I am trying to talk about more general concepts
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):for example, what is a library
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:16):what it means to depend on another library / theory?
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
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
Paolo Giarrusso (Nov 29 2020 at 23:17):I’m not sure I agree.
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):well, for example
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
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:17):that seems to me pretty much independent of dune
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
Paolo Giarrusso (Nov 29 2020 at 23:18):indeed, except that dune has its opinions :-)
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):any piece of code has an opinion of course
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):I don't see that as a bad thing
Paolo Giarrusso (Nov 29 2020 at 23:18):unclear, some code is more opinionated.
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:18):design by comittee worries me much more
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:19):in this case dune doesn't have an opinion on that
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:19):as it has little impact [5-10 lines of code]
Paolo Giarrusso (Nov 29 2020 at 23:19):today, in practice, it does.
Paolo Giarrusso (Nov 29 2020 at 23:19):but it keeps it to itself.
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:20):not sure I follow, anyways, got to go, see you tomorrow?
Paolo Giarrusso (Nov 29 2020 at 23:20):absolutely don’t let me keep you, can I reply asynchronously?
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:20):Sure
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).
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:25):The problem with the warnings is very different and happens under -Q
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):But I insist that Dune has no opinion on that yet
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.
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):It is implementing a version that imitates the OCaml smenatics
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):but the reason the issue you have just seen is still open
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):is that still is not clear what the opinion on that is
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:26):the issue is open well, because we recognize is an issue
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):however the solution is not simple due to other features, composition etc...
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):if dune had an opinion o that
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):on that, I'd close the issue as wontfix
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):however the answer is neither 'let's use -Q`
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:27):as that may brings some other problems
Paolo Giarrusso (Nov 29 2020 at 23:27):to be sure, we use “have an opinion” for different things
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
Paolo Giarrusso (Nov 29 2020 at 23:28):ah
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28):a bug is not an opinion
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28)::)
Emilio Jesús Gallego Arias (Nov 29 2020 at 23:28):what you point out is, as of today, an unresolved bug
Paolo Giarrusso (Nov 29 2020 at 23:28):whatever the intention, dune gives me -R, that’s all
Paolo Giarrusso (Nov 29 2020 at 23:28):at a high-level
Paolo Giarrusso (Nov 29 2020 at 23:29):I don’t want to alter my imports because I move my code across libraries.
Paolo Giarrusso (Nov 29 2020 at 23:29):I work on a “virtual monorepo” split into different repos
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.
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.
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
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.
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
Paolo Giarrusso (Dec 13 2020 at 22:03):I do mean with -R
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.
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
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):yeah, that doesn't work
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):but it is a good idea if it worked indeed
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:08):rules for qualified names are a different indeed in Coq
Paolo Giarrusso (Dec 13 2020 at 22:09):so maybe your -open proposal should make that work?
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
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:09):exactly
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
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
Paolo Giarrusso (Dec 13 2020 at 22:09):I'm uncertain myself, and this might warrant a CEP
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):I have a PR incoming so we may discuss a bit there
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
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):gather feedback, refine
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:10):and declare it stable when we are happy
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:11):CEPs may not do the best job anticipating all use cases here IMO
Emilio Jesús Gallego Arias (Dec 13 2020 at 22:11):and compatibility issues!
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...
Paolo Giarrusso (Dec 13 2020 at 22:11):fair point
Paolo Giarrusso (Dec 13 2020 at 22:12):indeed, IETF drafts must be implemented before standardization
Last updated: Jun 03 2023 at 17:29 UTC