Emilio Jesús Gallego Arias (Oct 23 2020 at 10:58): Emilio Jesús Gallego Arias (Oct 23 2020 at 10:58):@Karl Palmskog writes:
CoqHammer was one of the most challenging projects I've ever dunerized, and there the main developer prefers coq_makefile for local development going forward, so Dune maintenance will be challenging
What was exactly challenging about it? From a quick look I see nothing strange. Note that I think that recent Dune directly understand C and C++ executables, maybe you could take advantage of that? Also, it may be more convenient to actually declare .vo files as a test target instead of manually calling Coq.
Karl Palmskog (Oct 23 2020 at 11:01):as you might have seen, I had to preserve the coq_makefile build, which used .mllib
Emilio Jesús Gallego Arias (Oct 23 2020 at 11:01):But you switched to mlpack right?
Karl Palmskog (Oct 23 2020 at 11:01):the main challenge was in making the coq_makefile build and the Dune build completely equivalent
Karl Palmskog (Oct 23 2020 at 11:02):yes, in the end it seems to work now with mlpack
Emilio Jesús Gallego Arias (Oct 23 2020 at 11:02):I see, indeed keeping both build systems is 4x the work, not sure I'd recommend that
Karl Palmskog (Oct 23 2020 at 11:03):the maintainer has a fairly conservative style, so if I suggest a replacement, that PR was not likely to get merged
Karl Palmskog (Oct 23 2020 at 11:04):I still don't know how to specify .vo targets that should be invokable as if they were tests, i.e., something that can be triggered at the opam level with the -t option
Karl Palmskog (Oct 23 2020 at 11:05):CoqHammer has "smoke tests" that should be run but whose output should be completely ignored
Karl Palmskog (Oct 23 2020 at 11:08):finally, "challenging going forward" means that if some change to Makefile is done, one has to conjure up an equivalent in the Dune world
Emilio Jesús Gallego Arias (Oct 23 2020 at 11:30):Yeah, experience has shown that it is not a good idea to keep two build systems
Karl Palmskog (Oct 23 2020 at 12:21):@Emilio Jesús Gallego Arias but I think we have to choose between the following bad options:
using coq 1.0) is out (this leaves a huge "backlog")using coq 0.2 and keep coq_makefile around until 2.8 ("two build systems")to me, option 2 still seems preferable.
Paolo Giarrusso (Oct 23 2020 at 20:31):Does 2.8 fix other issues like IDE integration?
Karl Palmskog (Oct 23 2020 at 23:08):do we even have a definition of what a fully "fixed integration" means? To me at least, we need some way to have all of PG/VsCoq/CoqIDE automatically read Dune-built .vo files as indicated in _CoqProject, and for the same _CoqProject to work both with Dune and coq_makefile without changes
Karl Palmskog (Oct 23 2020 at 23:14):many people stumble into proper installs of Coq itself, which at least gives you coq_makefile. If we see projects switch to Dune and suddenly drop IDE support when building with coq_makefile, this would be bad for the ecosystem (everyone and their brother has to figure out how to install Dune and use dune build/dune build -p <name>)
Karl Palmskog (Oct 23 2020 at 23:16):for example, adding Dune across Linux/Mac/Win is seemingly not going to happen for the 8.12 platform: https://github.com/coq/platform/issues/11
Paolo Giarrusso (Oct 23 2020 at 23:35):for the same _CoqProject to work both with Dune and coq_makefile without changes
The plan I keep hearing is to replace _CoqProject by a better format.
Paolo Giarrusso (Oct 23 2020 at 23:36):I can guess sensible reasons, but I assume some backward compatibility
Karl Palmskog (Oct 23 2020 at 23:36):I have heard this as well, but I think I know the Coq ecosystem well enough now to estimate that a switch to something new instead of _CoqProject might take years
Paolo Giarrusso (Oct 23 2020 at 23:37):Oh sure
Paolo Giarrusso (Oct 23 2020 at 23:37):suddenly drop IDE support when building with coq_makefile
Coq's not Apple, but I'm sure I misunderstand :-)
Paolo Giarrusso (Oct 23 2020 at 23:38):still, _adding_ support for a _CoqProject alternative, without regressions, makes sense to me.
Karl Palmskog (Oct 23 2020 at 23:39):well, I mean "IDE support" in the sense of: you open emacs/code/coqide and it just works. Perhaps projects will be IDE+Dune by default, but there is some small change you can do to have IDEs+coq_makefile suddenly work again. This would still be bad.
Paolo Giarrusso (Oct 23 2020 at 23:40):I'd expect coq_makefile to stay the default.
Paolo Giarrusso (Oct 23 2020 at 23:40):in any case, Coq has sane deprecation policies.
Paolo Giarrusso (Oct 23 2020 at 23:40):and an extensive CI.
Karl Palmskog (Oct 23 2020 at 23:44):the last few comments in the following issue are unfortunately not encouraging w.r.t. reaching ideal IDE support: https://github.com/ProofGeneral/PG/issues/477
Paolo Giarrusso (Oct 23 2020 at 23:45):I do expect the "deprecation period" will need to be longer than usual — but before that discussion, the alternatives need to exist.
Paolo Giarrusso (Oct 23 2020 at 23:47):(taking a look at the issue)
Karl Palmskog (Oct 23 2020 at 23:47):personally, I find it depressing that PG developers want to keep their special Coq build support inside PG. This is yet another build system in the growing collection, that we can't even run in CI in a reasonable way
Paolo Giarrusso (Oct 23 2020 at 23:51):looking at https://github.com/ProofGeneral/PG/issues/477#issuecomment-612879449, I don't think you can blame PG for offering a better user experience.
Yes, but there are important features missing and there is the general problem, that dune cannot deduce dependencies, before the file has been saved. I am not sure, if it is desirable to save a file when Proof General processes a require command.
Paolo Giarrusso (Oct 23 2020 at 23:53):in any case, nothing in that issue suggests breakage to what works today. You'll need to switch for new features, but that's a different story.
Paolo Giarrusso (Oct 23 2020 at 23:54):AFAICT, it's not clear how to regain today's user-experience with dune.
Karl Palmskog (Oct 23 2020 at 23:55):to me, having this kind of stuff in _CoqProject is terrible, and there must be some sanctioned alternative:
-R _build/default/coq/ Xyz
oh we agree on that
Paolo Giarrusso (Oct 23 2020 at 23:55):but adding code to emacs to run dune coqtop foo.v seems acceptable
Paolo Giarrusso (Oct 23 2020 at 23:57):I'm not sure how you read what in the issue. AFAICT, the open question is how to adapt today's "special Coq build support inside PG".
Paolo Giarrusso (Oct 23 2020 at 23:58):without it, PG might go back to the inferior UX in CoqIDE/VsCoq (and not quite)
Karl Palmskog (Oct 23 2020 at 23:58):what I would like to see would be auto-discovery in _build/... based on what people currently write in _CoqProject for coq_makefile
Paolo Giarrusso (Oct 23 2020 at 23:58):for a proper solution, find out all the features they need, and integrate proper support for them.
Paolo Giarrusso (Oct 23 2020 at 23:59):well — _build/default isn't reliable
Paolo Giarrusso (Oct 23 2020 at 23:59):_build can live in a parent folder, and default can be replaced by something else
Karl Palmskog (Oct 24 2020 at 00:00):they can, but I would be fine if it just worked in most cases
Paolo Giarrusso (Oct 24 2020 at 00:00):I'm not sure why generating _CoqProject doesn't work, but I assume Emilio has some reason
Karl Palmskog (Oct 24 2020 at 00:01):if we generate _CoqProject for Dune, then it seems we suddenly have to generate it for coq_makefile as well
Paolo Giarrusso (Oct 24 2020 at 00:01):why? _CoqProject's an input for coq_makefile?
Paolo Giarrusso (Oct 24 2020 at 00:01):but can you say why you'd want auto-discovery?
Paolo Giarrusso (Oct 24 2020 at 00:02):the only "problem", if there is one, is that dune wants more info and in a more structured form. I assume that has valid reasons.
Paolo Giarrusso (Oct 24 2020 at 00:03):Since migration is not easy, all the existing code has to stay around for quite a while.
Karl Palmskog (Oct 24 2020 at 00:03):what I want is for projects to have the possibility to support the following out of the box, without any hacks:
Paolo Giarrusso (Oct 24 2020 at 00:03):okay
Paolo Giarrusso (Oct 24 2020 at 00:03):but then, why would you read _CoqProject for a dune project?
Paolo Giarrusso (Oct 24 2020 at 00:04):AFAICT, it contains a _projection_ of the info dune has.
Karl Palmskog (Oct 24 2020 at 00:05):Dune itself doesn't have to read _CoqProject
Paolo Giarrusso (Oct 24 2020 at 00:05):of course not.
Paolo Giarrusso (Oct 24 2020 at 00:06):and neither does the editor, no?
Karl Palmskog (Oct 24 2020 at 00:06):but in effect _CoqProject is the main signaler to CoqIDE and PG where things are found and should not have to be changed around with hacks (just because you pick one IDE or build system)
Paolo Giarrusso (Oct 24 2020 at 00:07):I agree the alternative shouldn't use hacks.
Paolo Giarrusso (Oct 24 2020 at 00:08):is the buried lede that hacks are unavoidable?
Karl Palmskog (Oct 24 2020 at 00:09):I'm not sure, but it only takes key developers being convinced that this is so [hacks are unavoidable] for it to become the case in practice
Paolo Giarrusso (Oct 24 2020 at 00:10):should not have to be changed around with hacks (just because you pick one IDE or build system)
Paolo Giarrusso (Oct 24 2020 at 00:11):do you want one standard interface between IDEs and build systems?
Karl Palmskog (Oct 24 2020 at 00:12):as a start, sure. But ideally we would have some Coq project metadata format that could not just be consumed by build systems and IDEs, but also by other tools
Paolo Giarrusso (Oct 24 2020 at 00:12):a standard interface seems unnecessary if the build systems are just the 2 ones, which seems everybody's working assumption...
Paolo Giarrusso (Oct 24 2020 at 00:12):... if you want something better, plausible approaches probably exist
Karl Palmskog (Oct 24 2020 at 00:13):our meta.yml in coq-community is just a convention after all, only used by our templates. Some of the data there in my opinion belongs elsewhere since it's so general.
Paolo Giarrusso (Oct 24 2020 at 00:14):Ah. You want a generic format for (Coq) IDE project files :-).
Paolo Giarrusso (Oct 24 2020 at 00:15):this was reminding me of Scala's Build Server Protocol (BSP), but this might be a different problem.
Karl Palmskog (Oct 24 2020 at 00:15):my main concern is actually analysis tools
Paolo Giarrusso (Oct 24 2020 at 00:16):I wonder what specific analyses you have in mind, but I can totally imagine nontrivial requirements.
Karl Palmskog (Oct 24 2020 at 00:17):opam files express some information about how to build a project, but not enough to do advanced stuff. _CoqProject sometimes gives a piece of the puzzle, but it's not standardized enough
Paolo Giarrusso (Oct 24 2020 at 00:18):and dune files still lack some info?
Karl Palmskog (Oct 24 2020 at 00:18):well, you would have to figure out if Dune even works
Paolo Giarrusso (Oct 24 2020 at 00:19):I have more questions about your requirements, but I'm not the actual target audience.
Paolo Giarrusso (Oct 24 2020 at 00:20):I totally agree this could be a significant undertaking, and it'd probably be ideal to collect all the requirements _before_ transitioning the whole ecosystem.
Paolo Giarrusso (Oct 24 2020 at 00:21):I still cannot tell if the "standardized format" would have to be dune files or sth else, but I suppose that's a million $ question.
Paolo Giarrusso (Oct 24 2020 at 00:23):all I can say: in my industrial team we'd want both jump-to-definition and async proofs, and we have 0 IDEs supporting that.
Karl Palmskog (Oct 24 2020 at 00:26):the kicker to me is not: async proofs inside IDEs. It's intelligent use of async proofs and parallelism in CI.
Paolo Giarrusso (Oct 24 2020 at 00:28):didn't your paper say that make -jX was enough CI parallelism?
Karl Palmskog (Oct 24 2020 at 00:31):make -jX can give you a one digit speedup, but more intelligent use of .vos/.vio and incrementality can give two digits speedup
Paolo Giarrusso (Oct 24 2020 at 00:31):and async proofs seem likely to have lower throughput in CI (which is why I only use it in IDE)
Paolo Giarrusso (Oct 24 2020 at 00:31):I mean, we'd kill for any CI speedup, but if we managed to use dune caching we'd be more than happy.
Paolo Giarrusso (Oct 24 2020 at 00:31):Most of our build is embarrassingly parallel, but for good results we had to do implement composition and incrementality by hand.
Karl Palmskog (Oct 24 2020 at 00:33):I still think binary caching is not the way to go, better to persist some simple metadata
Paolo Giarrusso (Oct 24 2020 at 00:33):make vos is also cool, but make vos; make vok is slower than make
Karl Palmskog (Oct 24 2020 at 00:33):not always, but in general, sure.
Paolo Giarrusso (Oct 24 2020 at 00:34):curious on that too, AFAICT dune's caching sounds a bit like bazel's
Paolo Giarrusso (Oct 24 2020 at 00:34):that runtime was on one project, after adding all needed Proof using./ Set Default... everywhere
Paolo Giarrusso (Oct 24 2020 at 00:34):minus on Program Obligations
Paolo Giarrusso (Oct 24 2020 at 00:36):anyway, I'll finally get https://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL18piCoq.pdf on my reading list
Karl Palmskog (Oct 24 2020 at 00:36):from my recollection, you can't easily control number of workers or scheduling with make vok
Paolo Giarrusso (Oct 24 2020 at 00:37):I thought there was just one thread? but I've never tried multithreaded proving
Karl Palmskog (Oct 24 2020 at 00:38):but anyway, my intuition is that the incrementality itself is the largest gain once you have basic make -jX vos or make -jX vio on an annotated codebase
Paolo Giarrusso (Oct 24 2020 at 00:38):at least in VsCoq, the overhead of delegating proofs seems terrible for throughput
Paolo Giarrusso (Oct 24 2020 at 00:38):right, that's true!
Paolo Giarrusso (Oct 24 2020 at 00:39):it's only sad the vos/vok files must be blown away by full builds :sad: :
Karl Palmskog (Oct 24 2020 at 00:39):"blown away"? you mean the combination make vos; make vok?
Karl Palmskog (Oct 24 2020 at 00:42):anyway, for CUDW I plan to try to revive an effort to get the votour program up to date so it can extract tons of interesting stuff from .vio/.vos useful for intelligent decisions after you have done your basic make -jX (ideally, even the first make -jX would not touch unaffected parts of the project)
Paolo Giarrusso (Oct 24 2020 at 00:45):re "blown away", running make will clear any .vos/.vok files, since they _could_ be stale.
Paolo Giarrusso (Oct 24 2020 at 00:46):(and leave them with size 0)
Karl Palmskog (Oct 24 2020 at 00:46):one thing that would be exciting is to actually use opacity information to rule out that some changes cannot affect other proofs (e.g., you write a definition with Qed, which means proofs using this definition cannot fail simply because you change the definition body)
Paolo Giarrusso (Oct 24 2020 at 00:46):I thought dune did that? Or does it just ignore changes to comments?
Karl Palmskog (Oct 24 2020 at 00:47):we did not do this [opacity analysis] in our papers, but it's a simple thing to do by modifying the Coq term dependency graph
Karl Palmskog (Oct 24 2020 at 00:47):Dune does not look at the term level at all currently, though Emilio has some experimental work in that direction I believe. I'm not even sure Dune uses intelligent hashing of files that ignores comments. The ideal would be to have Coq lex or parse the file and compute the hash based on the lex or parse output.
Karl Palmskog (Oct 24 2020 at 00:50):since it may be relevant, I will drop a paper where we looked specifically at Coq term-vs.-file dependency graphs, and how the incremental analysis works formally (incorporating opacity would be a small simple modification): http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL20Chip.pdf
Karl Palmskog (Oct 24 2020 at 00:51):if nothing else, it has good refs to build system research
Karl Palmskog (Oct 24 2020 at 00:56):the amazing thing in Coq, which means we should be blowing out test selection/parallelization in Java and the like out of the water, is that type checking is deterministic (and has predictable runtime, but this is just a cherry on top)
Paolo Giarrusso (Oct 24 2020 at 01:14):Not quite sure how type checking is less deterministic in Java... I’d also expect it to be faster in Java than Coq...
Paolo Giarrusso (Oct 24 2020 at 01:14):But I’ll have to read that paper first, I guess.
Karl Palmskog (Oct 24 2020 at 01:15):in Java, there is to my knowledge no way to rule out nondeterministic tests ("flaky tests"), most typically due to concurrency (but can also be due to use of external resources via network)
Paolo Giarrusso (Oct 24 2020 at 01:16):Ah! Okay, I get it.
Karl Palmskog (Oct 24 2020 at 01:17):flaky tests are a huge deal to, e.g., Google. It prevents you from trusting that "green" is "green".
Karl Palmskog (Oct 24 2020 at 01:19):the only near-equivalent in the Coq world we have is probably universe consistency, the checking of which can be deferred/avoided under certain circumstances, so Qed might not be full Qed
Karl Palmskog (Oct 24 2020 at 01:22):we proposed that projects that are paranoid about universe consistency could use vio2vo as a compromise, and load the resulting .vo files as a final step
Karl Palmskog (Oct 24 2020 at 01:31):unfortunately I don't think the same can be done for vos
Last updated: Jun 04 2023 at 23:30 UTC