Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Dune session

Paolo Giarrusso (Feb 15 2022 at 11:34):

Didn't find a topic here yet for dune

Emilio Jesús Gallego Arias (Feb 15 2022 at 13:10):

Indeed, thanks @Paolo Giarrusso

Emilio Jesús Gallego Arias (Feb 15 2022 at 13:10):

if you see the schedule we put it in a core slot as there was a lot of interest

Paolo Giarrusso (Feb 15 2022 at 13:36):

I added a few things under https://github.com/coq/coq/wiki/CoqWG-2022-02#a-preliminary-program-is-feel-free-to-add-your-topic. I labeled them as BedRock because I felt a bit bad about adding so many topics :-)

Emilio Jesús Gallego Arias (Feb 15 2022 at 13:37):

Great thanks!

Rodolphe Lepigre (Feb 16 2022 at 10:47):

I'm planning to spend a bit of time on trying to add something like dune coqtop (as I heard @Emilio Jesús Gallego Arias suggest at some point). This seems like the right thing to do to me, but it is also not completely trivial. I spent an hour or so looking into making a rough prototype, but I got quickly stuck on when trying to run a dummy version (just calling coqtop) from PG.

As far as I can tell, PG invokes coqtop following three variables: coq-prog-name (the program to invoke, does not accept arguments), coq-prog-args and coq-prog-env. What I did was set coq-prog-name to dune, and then add coqtop as first argument in coq-prog-args. However, this fails since PG keeps overwriting coq-prog-args (moving -emacs to first position). I'm not sure how to proceed form here: I was hoping to not have to hack PG at the same time...

Another question I have on the design of coqtop is: why does it not take care applying the options given in _CoqProject? To me, it seems a bit weird that the editors would each have to look for this file, and apply the arguments on their own. That seems like a work that could be shared rather easily, and the editors would only have to care about specific options (e.g., adding -emacs for PG).

Another issue I thought about is source code location when using dune: maybe there should be a generalised -Q PATH MOD_PATH option, say -QG SRC_PATH BUILD_PATH MOD_PATH which also maps the module path to where the compiled files are placed. This way, dune coqtop could simply set the paths correctly, and no hack would be required on the editor side.

(Some of the above was discussed by in https://github.com/ProofGeneral/PG/issues/477 at least, and some hack to strip the _build/default here https://github.com/cpitclaudel/company-coq/pull/257.)

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:47):

Hi @Rodolphe Lepigre , that's a superb project!

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:48):

I have a couple of pointers w.r.t. that, but I suggest we discuss them in the dune session

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:48):

I also have a tree with an skeleton implementation of dune coqtop

Rodolphe Lepigre (Feb 16 2022 at 10:48):

Sure, sounds good!

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:48):

will share later as I'm going for lunch now, and need to work a bit on my slides for the diversity session

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:49):

I will answer the rest of your questions later

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:49):

but for the arguments, dune already knows that to pass to them

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:49):

exactly, the idea is that you do dune coqtop foo.v and two things happne

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:49):

• the deps of foo.v are up to date (we could disable this with a flag, but it dosen't make sense in general)

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:50):

• coqtop is started with the right flags read from the dune file

Emilio Jesús Gallego Arias (Feb 16 2022 at 10:50):

the inspiration is from the way dune utop works

Paolo Giarrusso (Feb 16 2022 at 17:27):

For @Emilio Jesús Gallego Arias when you're back: do you still think there will be a dune hacking session tomorrow?

Emilio Jesús Gallego Arias (Feb 16 2022 at 17:27):

I will try to do the second part showing the implementation of the coqdoc rules

Emilio Jesús Gallego Arias (Feb 16 2022 at 17:27):

if it doesn't happen tomorrow

Emilio Jesús Gallego Arias (Feb 16 2022 at 17:27):

I will find a date next week and record it

Emilio Jesús Gallego Arias (Feb 16 2022 at 17:28):

or Friday

Emilio Jesús Gallego Arias (Feb 16 2022 at 17:28):

Scheduling needs work, ideas are welcome

MackieLoeffel (Feb 17 2022 at 08:28):

I would be interested in solving the issue described here: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Multi-package.20repositories But I don't really know enough dune to understand what exactly the problem is and how it could be fixed. @Emilio Jesús Gallego Arias Do you have some time to look into this together today or are you already fully booked?

Rodolphe Lepigre (Feb 17 2022 at 08:53):

Would you say this is more important than looking into proper editor support (i.e., the dune coqtop thing) @MackieLoeffel? If not, we could try looking at the dune coqtop thing together (hopefully with Emilio as well), and then try to fix the other issue once we get some more understanding of dune.

MackieLoeffel (Feb 17 2022 at 08:57):

I think dune coqtop / better editor support is more important than my issue. So If there is not enough time for both, I think it is better to look into dune coqtop. I would also be happy to help with dune coqtop.

Paolo Giarrusso (Feb 17 2022 at 09:03):

I'm coming in 5 minutes, but Emilio wrote he's away...

Rodolphe Lepigre (Feb 17 2022 at 09:05):

MackieLoeffel said:

I think dune coqtop / better editor support is more important than my issue. So If there is not enough time for both, I think it is better to look into dune coqtop. I would also be happy to help with dune coqtop.

My hope is that we can join efforts, and I need somebody that can help hack emacs and PG. And you know way more about these than I do. I hate emacs.

Rodolphe Lepigre (Feb 17 2022 at 09:06):

I'd say, let's meet in some breakout room 7. ;)

MackieLoeffel (Feb 17 2022 at 09:06):

I see. I am happy to help with emacs hacking. Let's join efforts then :+1: I'll be in the breakout room in a minute.

Janno (Feb 17 2022 at 09:21):

I've been looking into the PG issue and it seems that it overrides coq-prog-args with options extracted from _CoqProject if it finds that file. It also conses -emacs to that list, thus making it impossible to get any other first argument even when you modify _CoqProject by adding -arg.

Janno (Feb 17 2022 at 09:22):

Interestingly there are options in the code to skip that step (which would be annoying in many other ways) but the option is unused.

MackieLoeffel (Feb 17 2022 at 10:30):

We figured out how to call dune from emacs:

(setq coq-prog-name "opam")
(defun coq-prog-args-advice (res)
  `("exec" "--" "dune" "coqtop" ,buffer-file-name "--" "-emacs"))
(advice-add 'coq-prog-args :filter-return #'coq-prog-args-advice)

Kenji Maillard (Feb 17 2022 at 12:08):

This snippet looks worthy to be kept on the coq wiki but I don't find any page on dune.
Should there be a section getting started in the Coq FAQ listing this kind of advices ?

Rodolphe Lepigre (Feb 17 2022 at 12:13):

Turns out this does not quite work yet, but we'll indeed need to find where we want to put this. But we are still in the process of patching dune, so the proof general tweaks are not really useful to anyone but us yet.

MackieLoeffel (Feb 17 2022 at 12:14):

I adapted the snippet above such that it uses opam exec to find the right coqtop even when one has multiple switches. I needed to add another advice since proof general hardcodes coqtop in one place. Use with care, this might break at any time.

  ; setup proof general to use opam exec -- coqtop such that it always
  ; finds the right coqtop. Note that it does not help to override the
  ; coq-prog-args variable (not to be confused with the coq-prog-args
  ; function) as proof general calls the coq-prog-args function in the
  ; end and basically ignores the variable. So we advice the
  ; coq-prog-args function.
  (setq coq-prog-name "opam")
  (defun coq-prog-args-advice (res)
    ;; (message "coq-prog-args returned: %S" res)
    (append '("exec" "--" "coqtop") res))
  (advice-add 'coq-prog-args :filter-return #'coq-prog-args-advice)

  ; coq-callcoq uses only coq-prog-name and ignores coq-prog-args so
  ; we have to override it
  (defvar coq-callcoq-additional-args nil)
  (setq coq-callcoq-args '("exec" "--" "coqtop"))
  (defun coq-callcoq-advice (option &optional expectedretv)
    "Call coqtop with the given OPTION and return the output.
    The given option should make coqtop return immediately.
    Optionally check the return code and return nil if the check
    fails.  Return also nil on other kinds of errors (e.g., `coq-prog-name'
    not found).
    This function supports calling coqtop via tramp."
    (let ((coq-command (or coq-prog-name "coqtop"))
          retv)
      (condition-case nil
          (with-temp-buffer
            ; the following line is modified compared to the original
            (setq retv (apply 'process-file coq-command nil t nil
                              (append coq-callcoq-args (if option (cons option nil) nil))))
            (if (or (not expectedretv) (equal retv expectedretv))
                (buffer-string)))
        (error nil))))
  (advice-add 'coq-callcoq :override #'coq-callcoq-advice)

MackieLoeffel (Feb 17 2022 at 12:18):

Actually, there is a significantly simpler solution: Just create a file opam-coqtop with the following contents and put it into the path.

#!/bin/sh
opam exec -- coqtop "$@"

Then one just needs to do

  (setq coq-prog-name "opam-coqtop")

Paolo Giarrusso (Feb 17 2022 at 12:20):

but this script wouldn't work for dune coqtop, unless you parse cmdline args in shell to rearrange them, right?

MackieLoeffel (Feb 17 2022 at 12:22):

That depends on how dune coqtop expects its arguments. If it accepts the arguments the same way as coqtop it would work. Otherwise one would need to add some hacks to the shell script. But I see this as an argument why dune coqtop should accept the arguments in the same format as coqtop.

Paolo Giarrusso (Feb 17 2022 at 12:31):

That's not quite possible: at the very least, the caller shouldn't supply the -Q and -w options.

Paolo Giarrusso (Feb 17 2022 at 12:32):

so either you filter those out in shell, or you patch Proof General; I'd hope the original patch is enough for now, and for upstream or somebody with a clue to do the Emacs part properly :-)

MackieLoeffel (Feb 17 2022 at 12:33):

dune coqtop could also just ignore the additional options (maybe with a special flag on the commandline).

MackieLoeffel (Feb 17 2022 at 12:35):

But I don't know what the right option is.My feeling at the moment is that having a shell script (or python script) that filters out the options might be easier than patching PG but that is mostly because I've written more shell scripts than elisp.

Paolo Giarrusso (Feb 17 2022 at 12:37):

BTW I also posted the API question here: https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/Dune.20internals.3A.20build.20a.20target.20.60--only-deps.60

Paolo Giarrusso (Feb 17 2022 at 12:37):

I did it on the other stream in case the discussion exceeds the CoqWG

Paolo Giarrusso (Feb 17 2022 at 12:47):

oh @Emilio Jesús Gallego Arias is back! :-)

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:47):

Hi folks, yes I'm back!

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:47):

I had a long doctor appt this morning + lunch

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:48):

give me 10 minutes to catch up

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:48):

but see what I wrote in the jsCoq topic

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:48):

it seems to me that we could do a more thematic day

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:48):

half a day like "dune hacking day"

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:48):

schedule it some day, announce it, and focus solely on dune work

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:49):

because now as organizer I have a few things to do too, and I feel we got so many ideas as to cover them in a one hour breakout session

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:49):

but for sure let's try to do a breakout todya

Emilio Jesús Gallego Arias (Feb 17 2022 at 12:49):

even if just to start things

Tomás Díaz (Feb 17 2022 at 13:02):

Kenji Maillard said:

This snippet looks worthy to be kept on the coq wiki but I don't find any page on dune.
Should there be a section getting started in the Coq FAQ listing this kind of advices ?

Maybe this one could go in the environment setup doc?

Kenji Maillard (Feb 17 2022 at 13:09):

yep exactly, thanks for digging that page up, I added a link in the FAQ so that it's easier to access

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:16):

Ok I'm good if you folks wanna do a Dune breakout

MackieLoeffel (Feb 17 2022 at 13:17):

I would be available now as well. How about @Rodolphe Lepigre ?

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:19):

Ok let's go to room 2

MackieLoeffel (Feb 17 2022 at 13:19):

:+1: Give me one minute

Paolo Giarrusso (Feb 17 2022 at 13:21):

coming!

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:58):

@Rudi Grinberg , we have one question, we want to implement dune coqtop foo.v which basically builds all deps of foo.v and calls coqtop with the right flags.

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:59):

Does it make sense to add an alias @deps-foo.v as to implement the build deps step?

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:59):

Otherwise we could introduce like a file with the hashes, but seems strange

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:59):

or export directly the deps action, maybe that's best

Emilio Jesús Gallego Arias (Feb 17 2022 at 13:59):

?

Rudi Grinberg (Feb 17 2022 at 15:30):

why do you need the intermediate file or alias dependency at all?

Rodolphe Lepigre (Feb 17 2022 at 16:02):

When we run dune coqtop foo.v we need to make sure that all dependencies of foo.v are compiled.

Rodolphe Lepigre (Feb 17 2022 at 16:02):

(But we do not need to compile foo.v itself.)

Emilio Jesús Gallego Arias (Feb 17 2022 at 16:02):

folks let's move the discussion to the Dune subtopic as I see there are several topics

Emilio Jesús Gallego Arias (Feb 17 2022 at 16:03):

but indeed @Rudi Grinberg that's the reason

Rudi Grinberg (Feb 17 2022 at 16:03):

Sure, I can reply in the subtopic

Rodolphe Lepigre (Feb 17 2022 at 16:19):

@Emilio Jesús Gallego Arias would you have a bit of time to look into things with me? I think I just need some help to get started, I'm still quite confused about how dune works.

Rudi Grinberg (Feb 17 2022 at 17:06):

Is the hackathon in session now?

Emilio Jesús Gallego Arias (Feb 17 2022 at 17:08):

@Rodolphe Lepigre I have to leave now, my week got a bit unlucky due to many personal constraints

Emilio Jesús Gallego Arias (Feb 17 2022 at 17:08):

tomorrow too

Rodolphe Lepigre (Feb 17 2022 at 17:09):

No worries @Emilio Jesús Gallego Arias!

Emilio Jesús Gallego Arias (Feb 17 2022 at 17:09):

Next week I should have plenty of time, maybe Rudi is around tho, the rooms are open

Rodolphe Lepigre (Feb 17 2022 at 17:10):

Sure, if you are up to join the session @Rudi Grinberg we can perhaps have a chat in a breakout room?

Rodolphe Lepigre (Feb 17 2022 at 17:12):

I'm gonna go to room 7 just in case anyone wants to join.

Rudi Grinberg (Feb 17 2022 at 17:13):

ok let me join

Last updated: Jun 10 2023 at 23:01 UTC