Stream: CUDW 2020

Topic: Expert hotline

Yannick Forster (Nov 27 2020 at 14:41):

In the last years, one modus operandi for participation at CUDW / CIW was to just come, not participate in a working group / form a singleton working group and then use the unique possibility to have access to Coq developers once problems came up. I personally did this multiple times and found that a tremendously great way to learn things about the internals of Coq and to ask vague questions to experts and let them figure out how it was really meant. Do we have an idea how to simulate something like this in a remote setting? I.e. is there some way where you can shout "I need an expert" and then somebody pops up in a BBB breakout room?

Karl Palmskog (Nov 27 2020 at 14:46):

unless there is a BBB room, how about we just use this topic?

Théo Zimmermann (Nov 27 2020 at 14:49):

Yeah, I think it would make sense to just use this topic to shout for help and then, people can decide to join a specific breakout room together.

Yannick Forster (Nov 27 2020 at 15:13):

I think that's good enough. It would additionally be great if the initial session of the workshop could announce that there's the possibility to shout for help and somebody will turn up

Yannick Forster (Nov 27 2020 at 15:14):

And encourage as much as possible to shout, there's probably a large hesitation especially for first-time participants to actually shout for a Coq developer

Pierre-Marie Pédrot (Nov 27 2020 at 15:16):

Indeed.

Fabian Kunze (Nov 30 2020 at 10:16):

Is it expected that the ocaml-debugger does seemingly diverge when pretty-printinga relatively small terms of type ('a Glob_term.glob_constr_g) list?
I think i just have the list "[true]", which in the back is probably GApp CSTR.list_0.1 [...], but printing the argument list to the GApp does not work.
(I put a breakpont into constr_of_glob in notation.ml and calle Check [true]. in coq).

Fabian Kunze (Nov 30 2020 at 10:18):

(I worked around this issue, but it seemed strange)

Hugo Herbelin (Nov 30 2020 at 10:40):

That's probably the problem that Glob_term contains lazy values and ocamldebug is not robust enough to not hang when it has to print an unevaluated lazy value (a marshalling problem I guess).
My own solution is to never print a Glob_term unless we are sure it has already been evaluated, e.g. after an OCaml match.
Don't know if some people have better solutions.

Ana de Almeida Borges (Nov 30 2020 at 12:12):

Does anyone do Coq development with Spacemacs? Even though in the terminal I am using the master branch of Coq, it seems that inside spacemacs it is not being used.

Kenji Maillard (Nov 30 2020 at 12:13):

I do, but the coq version I use (including master) is bound to opam and I need to reload the opam env setting when I'm switching branch

Ana de Almeida Borges (Nov 30 2020 at 12:16):

I'd be happy to have that set up. Right now I am in an opam swich without Coq and am working on a clone of Coq master. I'm guessing that opam isn't aware of this. How could I enlighten it? Or could you just give me a pointer to your set up?

Kenji Maillard (Nov 30 2020 at 12:17):

In greater details, I define this hackish elisp function in dotspacemacs/user-init for retrieving opam's current environment (I really don't know much about elisp/emacs so that code might be really bad):

  (defun load-opam-env ()
    (mapc
     (lambda (s)
       (let ((r (split-string s "=")))
         (setenv (car r) (cadr r))))
     (split-string (shell-command-to-string "opam env --shell=bash | sed -e 's/;.*;/;/'")))

And then call (load-opam-env) in dotspacemacs/user-env

Kenji Maillard (Nov 30 2020 at 12:18):

you can install coq's master in opam by pinning the directory of coq

Kenji Maillard (Nov 30 2020 at 12:18):

from the top directory of Coq's sources, you should be able to do something like opam install . --pin I think

Kenji Maillard (Nov 30 2020 at 12:19):

This should be documented somewhere but I'm not sure where...

Kenji Maillard (Nov 30 2020 at 12:22):

Probably something should be added either to https://github.com/coq/coq/blob/master/CONTRIBUTING.md#building-coq or https://github.com/coq/coq/blob/master/INSTALL.md
Currently there is no indication on how to setup a reasonable working environment...

Kenji Maillard (Nov 30 2020 at 12:25):

even https://github.com/coq/coq/blob/master/dev/doc/README.md falls short proposing any potential/typical environment for developping on Coq...

Ana de Almeida Borges (Nov 30 2020 at 12:27):

I did opam pin coq . from the correct directory, and that gave me an error... Intuitively I would expect this to have worked, and possibly the error is related to Coq and not to opam?

coq is now pinned to git+file:///home/ana/coq#master (version dev)

The following actions will be performed:
  ∗ install coq dev*
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq failed at "/home/ana/.opam/opam-init/hooks/sandbox.sh build dune subst".

#=== ERROR while compiling coq.dev ============================================#
# context     2.0.5 | linux/x86_64 |  | pinned(git+file:///home/ana/coq#master#0ae001ee)
# path        ~/.opam/CoqMaster/.opam-switch/build/coq.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune subst
# exit-code   1
# env-file    ~/.opam/log/coq-1886824-d8a4ae.env
# output-file ~/.opam/log/coq-1886824-d8a4ae.out
### output ###
# Error: "test-suite/misc/deps/\316\261\316\262/\316\263\316\264.v": No such
# file or directory

Ana de Almeida Borges (Nov 30 2020 at 12:28):

I believe one of the plenary sessions is going to be precisely about how to set up an environment for development

Karl Palmskog (Nov 30 2020 at 12:29):

@Ana de Almeida Borges you probably don't want to pin the opam files in the GitHub Coq repo. Instead, consider using the core-dev opam repo: https://github.com/coq/opam-coq-archive/tree/master/core-dev

Karl Palmskog (Nov 30 2020 at 12:30):

if you're developing something, you probably want to build directly and not via opam

Ana de Almeida Borges (Nov 30 2020 at 12:32):

Thanks, I didn't know that repo existed. What is the difference from the regular one?

Kenji Maillard (Nov 30 2020 at 12:32):

Karl Palmskog said:

if you're developing something, you probably want to build directly and not via opam

I'm frequently developing/building directly and installing it in opam, is that a bad setup ?

Karl Palmskog (Nov 30 2020 at 12:33):

I'm not sure what is guaranteed about the .opam files that live in the Coq GitHub repo, but they are not tested outside of Coq's CI

Karl Palmskog (Nov 30 2020 at 12:34):

for a given opam switch, I would make a decision whether to build+install Coq directly or use Coq from core-dev

Karl Palmskog (Nov 30 2020 at 12:35):

Ana de Almeida Borges said:

Thanks, I didn't know that repo existed. What is the difference from the regular one?

The regular opam repo only has released versions of Coq. Those do not come from Git, while those in core-dev may come from Git (betas do not)

Ana de Almeida Borges (Nov 30 2020 at 12:36):

Oh, so the repo you linked is an actual thing that can be installed from opam!

Karl Palmskog (Nov 30 2020 at 12:37):

"installed from opam" can have many meanings, but yes, you can use core-dev packages with other packages, I use them to test Coq projects with alpha/beta versions of Coq, e.g., I have switch with coq.8.13.dev which is effectively 8.13+alpha

Ana de Almeida Borges (Nov 30 2020 at 12:40):

Alright. But if I'm making changes on top of the most recent (unreleased) version and then want to compile my changes, wouldn't I necessarily need to make locally? Or is the idea that I push my changes to a branch in the dev repo and then ask opam to recompile?

Kenji Maillard (Nov 30 2020 at 12:41):

Karl Palmskog said:

I'm not sure what is guaranteed about the .opam files that live in the Coq GitHub repo, but they are not tested outside of Coq's CI

That's a good point, but then isn't that a shortcoming of current infrastructure ? At least there should be some way to set up a developping environment using the usual tools and not hacking PATH environment all the time, no ?

Théo Zimmermann (Nov 30 2020 at 12:42):

I don't really recall how it works, but when I hack Coq, I can start Emacs with PG and get it automatically pick my Dune-based Coq build.

Théo Zimmermann (Nov 30 2020 at 12:42):

(without installing anything)

Karl Palmskog (Nov 30 2020 at 12:43):

right, for local Coq devolopment (as opposed to regular use) I would take opam out of the equation and either rely on Dune or make to build/install

Théo Zimmermann (Nov 30 2020 at 12:43):

Oh, that's probably because I import this: https://github.com/coq/coq/blob/master/dev/tools/coqdev.el

Théo Zimmermann (Nov 30 2020 at 12:44):

Karl Palmskog said:

right, for local Coq devolopment (as opposed to regular use) I would take opam out of the equation and either rely on Dune or make to build/install

:+1: except I wouldn't ever install

Emilio Jesús Gallego Arias (Nov 30 2020 at 12:47):

@Ana de Almeida Borges unfortunately you are hitting a Dune bug; it is fixed in the next dune version, for now the workaround is to edit the opam file and remove the susbt line.

Ana de Almeida Borges (Nov 30 2020 at 12:47):

Karl Palmskog said:

right, for local Coq devolopment (as opposed to regular use) I would take opam out of the equation and either rely on Dune or make to build/install

That makes sense, but then I'm back to my first question of making Spacemacs use the in-development version of Coq. Perhaps coqdev.elwill magically solve this issue, and otherwise I can try Kenji's suggestion with the Dune bug fix Emilio just brought up!

Kenji Maillard (Nov 30 2020 at 13:14):

Théo Zimmermann said:

Oh, that's probably because I import this: https://github.com/coq/coq/blob/master/dev/tools/coqdev.el

:hushed: I was not aware of this...
Can someone explain briefly what it provides ? The description in the dev/'s Readme is rather succint

Kenji Maillard (Nov 30 2020 at 13:16):

Also this seems to work for hacking on Coq. How do you usually develop your libraries depending on this hacked Coq ? My typical usage is testing new features such as SProp at some point, inductive-inductive today, ...

Ana de Almeida Borges (Nov 30 2020 at 20:23):

Kenji Maillard said:

In greater details, I define this hackish elisp function in dotspacemacs/user-init for retrieving opam's current environment (I really don't know much about elisp/emacs so that code might be really bad):

  (defun load-opam-env ()
    (mapc
     (lambda (s)
       (let ((r (split-string s "=")))
         (setenv (car r) (cadr r))))
     (split-string (shell-command-to-string "opam env --shell=bash | sed -e 's/;.*;/;/'")))

And then call (load-opam-env) in dotspacemacs/user-env

I just spent a fun afternoon trying to make something work and (after having broken several previously working things), I seem to be in a situation where I have to call tuareg-opam-update-env at the start of any emacs session (even with opam swiches with "regular" versions of Coq), which I didn't have to do previously at all.

I thought that was the point of load-opam-env(there is a missing ) in its definition btw), but it appears not to be working for me. When you say to call (load-opam-env), does that mean something other than adding a line with (load-opam-env) in dotspacemacs/user-env?

Kenji Maillard (Nov 30 2020 at 20:32):

I just call (load-opam-env) after (spacemacs/load-spacemacs-env) so that it's not overwritten, but I would also need to call it after changing switch. There is probably a better way to organize that...

Ana de Almeida Borges (Nov 30 2020 at 20:41):

I can't seem to find (spacemacs/load-spacemacs-env) other than in .emacs.d/core/..., and that doesn't look like the right place to configure things. Do you have that line in your .spacemacs?

Paolo Giarrusso (Nov 30 2020 at 20:42):

(spacemacs/load-spacemacs-env) is indeed not something you should change

Paolo Giarrusso (Nov 30 2020 at 20:43):

the one to customize is dotspacemacs/user-env

Paolo Giarrusso (Nov 30 2020 at 20:44):

@Ana de Almeida Borges I assume you’re using spacemacs develop, right?

Kenji Maillard (Nov 30 2020 at 20:44):

I'm really just following the default comment that is in my .spacemacs

(defun dotspacemacs/user-env ()
  "Environment variables setup.
This function defines the environment variables for your Emacs session. By
default it calls `spacemacs/load-spacemacs-env' which loads the environment
variables declared in `~/.spacemacs.env' or `~/.spacemacs.d/.spacemacs.env'.
See the header of this file for more information."
  (spacemacs/load-spacemacs-env)
  ;; Reloading the current opam env
  (load-opam-env)
  )

Ana de Almeida Borges (Nov 30 2020 at 20:44):

Paolo Giarrusso said:

Ana de Almeida Borges I assume you’re using spacemacs develop, right?

Yes I am

Paolo Giarrusso (Nov 30 2020 at 20:44):

reasonably up-to-date?

Paolo Giarrusso (Nov 30 2020 at 20:45):

do you use the commands to update .spacemacs from its template?

Paolo Giarrusso (Nov 30 2020 at 20:45):

(IIRC SPC f e D)

Ana de Almeida Borges (Nov 30 2020 at 20:45):

it used to be horribly out-of-date, but today I decided it would be a good idea to update it. So it's very up to date, but on the whole everything is working worse than before I updated it, so I'm regretting that decision...

Paolo Giarrusso (Nov 30 2020 at 20:45):

the “default comments” like the above won’t be upgraded automatically

Paolo Giarrusso (Nov 30 2020 at 20:46):

ah

Paolo Giarrusso (Nov 30 2020 at 20:47):

I mean, I’ve used spacemacs for a long time, but it does have the stability of duct tape

Paolo Giarrusso (Nov 30 2020 at 20:48):

“move faster and breaker morer thingser”

Ana de Almeida Borges (Nov 30 2020 at 20:48):

Ok, I don't even have a user-env in my .spacemacs, so probably what happened is that I updated everything but .spacemacs, and I even know how it happened (it had an error so I rolled it back to a saved version, but probably rolled too much back)

Kenji Maillard (Nov 30 2020 at 20:52):

Sorry I didn't think about that when throwing these lines of elisp (I also had some hard times once or twice with spacemacs update, so I'm doing it so rarely that I forgot about it...)

Ana de Almeida Borges (Nov 30 2020 at 21:51):

Sure, I also didn't think about it. In fact every time I try to change something in spacemacs I end up breaking it, and thus I am afraid of updating. Still, I should probably do it once in a while.

Ana de Almeida Borges (Nov 30 2020 at 21:56):

Right now I have the most recent version of emacs develop, a .spacemacs that looks very similar to the current template (with some changed options and added commands), the definition of load-opam-env in dotspacemacs/user-init, and a call to it in dotspacemacs/user-env. However, it still seems to not work.

When I open a Coq file and try to load compiled libraries it complains about a bad magic number. If I call tuareg-opam-update-env it works as expected. This was a step I didn't use to have to do before today. Am I right in thinking this is precisely the reason you, @Kenji Maillard , defined load-opam-env in the first place? Or was it just to use Coq dev?

Kenji Maillard (Nov 30 2020 at 22:54):

The load-opam-env is mainly to synchronized emacs PATH variable with the data of the current opam switch and tuareg-opam-update-env is probably doing the same. I think that coqtop and the path to the relevant coq libraries is then determined from that. In your case there seems to be something in the way. Do you have an a globally installed coq (outside opam) that could happen to be caught by a default PATH variable ?

Ana de Almeida Borges (Nov 30 2020 at 23:10):

Do you have an a globally installed coq (outside opam) that could happen to be caught by a default PATH variable ?

Great guess! It appears that I have a /usr/local/bin/coqtop, with Version 8.13+alpha. I probably installed it the last time I played around with Coq master a couple of months ago. I'm sorry for my ignorance, but what is the right way of getting rid of it? I assume rm /usr/local/bin/coqtop is too hacky?

Ana de Almeida Borges (Nov 30 2020 at 23:48):

I've hackily removed /usr/local/bin/coqtop for now and emacs is able to correctly pick the right version of Coq, just like it did last weekend! :)

As for my original problem, I did opam pin coq . and as far as I can tell it installed the dev version of Coq, but not my modified one (why?). So... I just added ~/coq/bin (the local dev version I'm messing around with) to the PATH. Is that a terrible idea? It works!

Paolo Giarrusso (Dec 01 2020 at 01:52):

Why not your changes: have you committed them? Opam will ignore uncommitted changes by default.

Yves Bertot (Dec 01 2020 at 08:49):

I developed a modification to the simpl tactic as an attempt to fix issue https://github.com/coq/coq/issues/13428 This is PR https://github.com/coq/coq/pull/13448 .
I needed 1: to add a new function in the ReductionBehaviour interface to obtain all functions that have the NeverUnfold flag (the one set by Arguments ... : simpl never.
2: to expose a function in the interface of reductionops.mli stack_red_of_state_red so that whd_state_gen could be transformed into a stack enabled reduction function.
Does that sound legitimate?
The remaining work is to setup a table storing all functions with the NeverUnfoldflag, to avoid traversing the full reduction behaviour table several time each time the tactic simpl is called.

Ana de Almeida Borges (Dec 01 2020 at 08:49):

Opam will ignore uncommitted changes by default

Huh. I had no idea. Thanks!

Adrian Dapprich (Dec 01 2020 at 12:12):

Hello, I was wondering if there is a way to construct tactics in ocaml and print them out (e.g. create some variable which represents the congruence tactic and which would print "congruence." when given to some kind of pretty printer). The reason is that I'm currently constructing definitions/lemmas etc with vernac_exprs and constr_exprs and printing them out to generate parseable coq code.
And while I don't need tactics for the most part, some lemmas can be proved with a single congruence and I wanted to try that out. But from what I gather from the plugin tutorials, the command "congruence" just triggers execution of a function which then changes the goal so there is no internal representation of a "congruence object" that I could print, right?
(Also is it then correct to say that tactics are not "reified"?)

Pierre-Marie Pédrot (Dec 01 2020 at 12:15):

@Adrian Dapprich Depends exactly at what level you live.

Pierre-Marie Pédrot (Dec 01 2020 at 12:16):

There is an AST of tactic expressions that can be printed.

Pierre-Marie Pédrot (Dec 01 2020 at 12:16):

But once you evaluate that AST you essentially get a blob.

Pierre-Marie Pédrot (Dec 01 2020 at 12:17):

IIUC your post you're only manipulating syntax, so you could build your tactic and print it. (And also discover a lot of printing bugs, as @Lasse realized the hard way.)

Pierre-Marie Pédrot (Dec 01 2020 at 12:19):

The tactic AST lives in plugins/ltac/tacexpr.mli, and the printers are in plugins/ltac/pptactic.mli, specifically pr_glob_tactic and pr_raw_tactic

Lasse Blaauwbroek (Dec 01 2020 at 12:22):

Most of the printing bugs are probably gone by now :-) Only ssreflect is still somewhat problematic.

Adrian Dapprich (Dec 01 2020 at 12:45):

@Pierre-Marie Pédrot thanks I had a look at these files and it appears I can then print the tactic when I take the correct index of the LTAC EXTEND declaration. But what I don't understand is the term "globalization". What does that mean? From looking through lib/genarg.mli and plugins/ltac/tacintern.ml it seems related to "interning" but I don't have an intuition for that either.

Pierre-Marie Pédrot (Dec 01 2020 at 12:45):

An AST in Coq typically goes through 3 phases: raw, glob, and top

Adrian Dapprich (Dec 01 2020 at 12:46):

Is it something like connecting things to the environment (like when I type the raw expression nat, it then gets connected to the nat from the stdlib)?

Pierre-Marie Pédrot (Dec 01 2020 at 12:46):

Raw is essentially what the user writes, glob is the same stuff with resolution of names and some other static data, and top is the toplevel value

Adrian Dapprich (Dec 01 2020 at 12:55):

ok thanks, so for terms that is the (constr_expr --> glob_constr --> econstr) pipeline. And for tactics I will probably also want to stay at raw expressions since I print then anyways

Emilio Jesús Gallego Arias (Dec 01 2020 at 13:01):

@Adrian Dapprich , if you need faithful printing of tactic's AST you are gonna have quite a few pain points.

Emilio Jesús Gallego Arias (Dec 01 2020 at 13:01):

I know because I implemented serialization of tactics AST in SerAPI, which maybe would help you

Emilio Jesús Gallego Arias (Dec 01 2020 at 13:02):

That was tested on a large codebase and it works in roundtrip

Yves Bertot (Dec 03 2020 at 09:56):

How do I know what is executed in ci-coq_performance_tests ? My PR has a failure at this test, I don't know how to reproduce it on my machine.

Théo Zimmermann (Dec 03 2020 at 10:20):

That's https://github.com/coq-community/coq-performance-tests

Théo Zimmermann (Dec 03 2020 at 10:21):

Note that for any such CI test, you can use make -f Makefile.ci ci-foo to get a local git clone of the source repo under _build_ci/.

Yves Bertot (Dec 03 2020 at 10:22):

Yes! your extra remark is what I was looking for!

Yves Bertot (Dec 03 2020 at 10:30):

Note that the git clone operation is extremely slow, it would be sensible to use the --depth 1 option in this process. this would gain a lot of time, wouldn't it?

Fabian Kunze (Dec 03 2020 at 10:35):

Should I rebase squash a PR to not contain "small" commits that e.g. fix typos in the doc?
is this done automatically by coqbot?

Fabian Kunze (Dec 03 2020 at 10:38):

Or more relevant, commits that improve on the code by incorporating the review. To avoid having "bad" intermediate code states and irrelevant git-blame-lines in the master branch.

Théo Zimmermann (Dec 03 2020 at 10:39):

Yves Bertot said:

Note that the git clone operation is extremely slow, it would be sensible to use the --depth 1 option in this process. this would gain a lot of time, wouldn't it?

Possibly. We don't use git to clone by default on the CI... @Gaëtan Gilbert should be able to comment more on this.

Théo Zimmermann (Dec 03 2020 at 10:40):

Fabian Kunze said:

Or more relevant, commits that improve on the code by incorporating the review. To avoid having "bad" intermediate code states and irrelevant git-blame-lines in the master branch.

Yes, please do squash commits that improve on the code introduced by the same PR. Do not hesitate to do multiple small commits for independent fixes to the code before the PR.

Gaëtan Gilbert (Dec 03 2020 at 10:41):

I looked a bit into it because hott is really terrible for this
IIRC we have to figure out whether we may use --depth (if the ref is a hash we can't) and I didn't have the motivation

Fabian Kunze (Dec 03 2020 at 11:21):

Does an ocamlexpert have an Idea why this code compiles fine under ocaml 4.10, but not under gitlab (ocaml 4.05).
I don't understand why the pattern forces 'a to unit:

let _ = function CPrimitives.(PTE(PT_int63|PT_float64|PT_array)) -> () in
Error:

File "kernel/environ.ml", line 591, characters 36-44:
Error: This pattern matches values of type unit CPrimitives.prim_type
       but a pattern was expected which matches values of type
         $PTE_'a CPrimitives.prim_type
       Type unit is not compatible with type $PTE_'a

Pierre-Marie Pédrot (Dec 03 2020 at 11:22):

Looks like a change in GADT typing.

Pierre-Marie Pédrot (Dec 03 2020 at 11:22):

the branches don't have the same type

Pierre-Marie Pédrot (Dec 03 2020 at 11:22):

It was a painful limitation that was lifted in some recent release

Pierre-Marie Pédrot (Dec 03 2020 at 11:23):

you have to pattern-match separately on each constructor.

Pierre-Marie Pédrot (Dec 03 2020 at 11:23):

int63 and float64 have the same type so they can remain together

Fabian Kunze (Dec 03 2020 at 11:23):

thanks for the explaination and proposed solution:)

Enrico Tassi (Dec 03 2020 at 12:19):

phew, dependent types...

Adrian Dapprich (Dec 03 2020 at 14:09):

Emilio Jesús Gallego Arias said:

Adrian Dapprich , if you need faithful printing of tactic's AST you are gonna have quite a few pain points.

If by faithful printing you mean actually printing the gen_tactic_expr AST as I think it happens in SerAPI, then no. I was just interested in printing the actual command "congruence" (or other tactics) and thereby printing a script which could be read in again by coqc/coqtop. I guess communicating with coq is probably better using SerAPI or other protocols but I was just curious.

Karl Palmskog (Dec 04 2020 at 11:34):

@Enrico Tassi do you have time to chat briefly in BBB on some opam packaging stuff before 15:00 today? Should not be more than 10 minutes.

Enrico Tassi (Dec 04 2020 at 11:35):

what about now?

Karl Palmskog (Dec 04 2020 at 11:36):

sure, works, let's use room 2

Enrico Tassi (Dec 04 2020 at 13:24):

@Gaëtan Gilbert @Emilio Jesús Gallego Arias how is dune running the tests?
test-suite/Makefile exports BIN so that scripts in test-suite/misc/ know where to find Coq binaries. On dune this variable is empty.

Enrico Tassi (Dec 04 2020 at 13:24):

How can I fix this?

Enrico Tassi (Dec 04 2020 at 13:25):

the test-suite/Makefile does set it to something sensible if coq was compiled with dune. If I run that makefile by hand it works. but if I use Makefile.dune (as the ci job I guess), then another code path is followed and BIN is not set

Gaëtan Gilbert (Dec 04 2020 at 13:27):

something in test-suite/dune I guess
Emilio probably knows more

Enrico Tassi (Dec 04 2020 at 13:28):

we have 2 build systems, but 3 ways of running the tests suite, :crazy:

Enrico Tassi (Dec 04 2020 at 13:29):

you are right!

 (action
  (progn
   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"

Enrico Tassi (Dec 04 2020 at 13:29):

:rage: BIN=

Enrico Tassi (Dec 04 2020 at 13:29):

Now the question is... why?

Enrico Tassi (Dec 04 2020 at 13:30):

I will fix it, but it seems it was done on purpose no?

Enrico Tassi (Dec 04 2020 at 13:31):

look at the code for COQLIB (which is indeed set correctly)

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:02):

I am pretty far with replacing this hackery with a proper dune file for the test suite

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:02):

In dune, you assume that the right coqc is in path

Gaëtan Gilbert (Dec 04 2020 at 14:02):

pr tomorrow?

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:02):

no

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:03):

You didn't say what your problem is so hard to know more

Gaëtan Gilbert (Dec 04 2020 at 14:03):

;_;

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:03):

but it seems whatever you are doing the right coqc is not in path

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:03):

there was some other hackery to actually allow running the test suite outside of dune, but IMHO that's a bad idea, there are many things to do to properly setup the env

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:04):

the PR is already there, it needs pushing

Enrico Tassi (Dec 04 2020 at 14:08):

I fixed it as part of https://github.com/coq/coq/pull/13523

Enrico Tassi (Dec 04 2020 at 14:09):

note that test-suite/Makefile passes explicitly BIN to the shell scripts, so the empty string is not an acceptable value

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:10):

Umm, that seems broken, why is BIN passed to shell scripts

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:11):

I thought they should use the $coqc variables etc...

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:11):

defined in the main makefile

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:13):

Yeah I'm not sure I'm a fan of .sh scripts having to manipulate the path

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:14):

yeah from a quick look it looks that the bug is in the scripts manipulating the path, not the other way around, IMHO they got no bussiness doing that

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:14):

what do you think @Gaëtan Gilbert

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:14):

seems pretty error prone to write tests this way

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:17):

Honestly that coq_enviroment stuff looks like a mess we will pay dearly for

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:17):

why can't the platform just set the right env vars?

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:17):

Surely on windows that's possible to do

Enrico Tassi (Dec 04 2020 at 14:23):

Emilio Jesús Gallego Arias said:

why can't the platform just set the right env vars?

Setting an env var on windows is not an option.

Enrico Tassi (Dec 04 2020 at 14:26):

Emilio Jesús Gallego Arias said:

Yeah I'm not sure I'm a fan of .sh scripts having to manipulate the path

My initial try was cp $coqc .. One day later, and 25 git push -f, I found that cp $BIN/coqc was working fine on all OS.
But for the dune job. I don't care which is the nice solution, but having only the dune job work differently is a problem.

Enrico Tassi (Dec 04 2020 at 14:27):

If you want to remove $BIN from test-suite, fine, but do it for all ways we run it.

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:28):

I guess the current status is fine; but I'm worried that every time I look at the windows stuff, the amount of mess is higher, not less

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:28):

already all relative to windows is non-standard they even have their own build system / logging [which is impossible to read] etc...

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:28):

so we add more and more mess I dunno

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:29):

already this con_env stuff seems suspicous

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:29):

I will write a comment in the PR

Gaëtan Gilbert (Dec 04 2020 at 14:29):

I'm staying away from that PR, it scares me

Enrico Tassi (Dec 04 2020 at 14:30):

We now build with opam

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:30):

Oh I see

Enrico Tassi (Dec 04 2020 at 14:30):

(in the patform)

Enrico Tassi (Dec 04 2020 at 14:30):

the ci job is still a mess, but shall be removed

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

You need the file for OCaml path

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

the suspicous part was that already, if you use Sys.executable_name

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

Coq already derives coqlib as you noticed

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

so you need to tweak ocamlfind

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

but IMHO the whole apporach is wrong

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

you should install the proper ocamlfind config file right?

Emilio Jesús Gallego Arias (Dec 04 2020 at 14:31):

so that PR should be dropped in favor of updating ocamlfind config?

Last updated: Apr 20 2024 at 00:02 UTC