Stream: Coq devs & plugin devs

Topic: test-suite + dune


view this post on Zulip Ali Caglayan (Mar 01 2022 at 17:43):

When I do dune runtest make seems to have a low number for -j, is there a way I can hack it to use my dune jobs env var?

view this post on Zulip Ali Caglayan (Mar 01 2022 at 17:44):

I know there is a wip port of the test-suite to dune, but I am looking for short term solutions

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 17:53):

I'm afraid not a short term other than tweaking NJOBS env var

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 17:54):

See the rule in test-suite/dune

view this post on Zulip Ali Caglayan (Mar 01 2022 at 21:55):

OK tweaking NJOBS works

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):

I suggest we use this thread to discuss about the test-suite PR

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):

@Ali Caglayan

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):

I did rebase and things seem OK except for a couple of issues

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:53):

Yep my rebase looked pretty similar

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:53):

The META stuff I think can be fixed by passing the correct -I right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):

It runs fine on my computer with dune build @test-gen

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):

then dune runtest

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:54):

Does runtest not call test-gen?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:54):

Ali Caglayan said:

The META stuff I think can be fixed by passing the correct -I right?

I don't know, I would worry about that last, as maybe some other PR we have scheduled fixes it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:54):

Ali Caglayan said:

Does runtest not call test-gen?

Not in the current version, I'm not sure if Dune 3.0 still allows that, or it was postponed to 3.1

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:54):

But we can do a little make rule as I did here

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:54):

OK so the coq-core.plugins.ltac can be fixed by changing it to ltac_plugin

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:55):

But there is a syntax error from coqdep in bugs/12138

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:55):

https://github.com/coq/coq/pull/15560/files#diff-67a1b30447bd9ee29ddc18999eaaa4d13da7af1e7e5267a5829dcefb86b6824eR108

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:55):

Ali Caglayan said:

But there is a syntax error from coqdep in bugs/12138

Yes, I did remove it for now

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:55):

So I moved it to a seperate folder where we won't call coqdep on tests

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:55):

we need to fix coqdep

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:55):

Fixing coqdep is tricky though because it uses . for terminals but the test has {.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:56):

I see, I guess we'll figure out a compromise.

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:57):

My fix for the META stuff is just a work around however

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:57):

We need to pass -I correctly to coqdep for this to work

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:58):

currently we are only passing ltac

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:58):

I wanted to maybe copy what is being done in the shims but I don't really understand that

view this post on Zulip Ali Caglayan (Mar 02 2022 at 11:58):

let cctx =
  [| "-I"; "../plugins/ltac"
   ; "-R"; "../theories" ; "Coq"
   ; "-R"; "prerequisite"; "TestSuite"
   ; "-Q"; "../user-contrib/Ltac2"; "Ltac2" |]

This seems wrong for example, I thought we had better ways of getting this info?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 11:59):

@Ali Caglayan this is hardcoded for now, but it doesn't look wrong to me

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):

eventually we may use a dune file

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:00):

Right, but should we be looking in install?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):

with (coq.theories ...)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):

Ali Caglayan said:

Right, but should we be looking in install?

what do you mean?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):

IMHO we shouldn't touch install

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:01):

    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")

this is from the shim

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:01):

unless we want to add a flag for running the test suite vs an installed Coq, but I don't see the use case

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:01):

Ali Caglayan said:

    (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")

this is from the shim

that was introduced in the findlib PR?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):

if so we want to fix it, but there was some problem

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):

so that's like a temporary solution I think

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):

we could use it here too, but I think the problem was due to the META file being not in the right place, but we will find the right way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):

but it could involve patching dune or findlib

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):

I propose we look at this last

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):

as I have some fixes pending for the META stuff

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):

so use install or whatever works best for you

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:05):

There is also a small problem with the rule generation

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:05):

Ali Caglayan said:

There is also a small problem with the rule generation

tell me

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:06):

If there is an excpetion, such as the ones we currently get, we get an unbalanced sexp

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:06):

I have to keep fixing it with a closing paranthesis

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):

yes, that's a pain, I have to do rm + touch

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):

indeed I propose we add to gen_rules a clean setp

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):

that truncates the file if an exception

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):

or your fav workaround

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:07):

I'm going for lunch, the tree is fully yours

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:07):

Is it too hacky to just add a brace at the end?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:07):

I would just truncate the file on the exception handler, seems simpler, as we may be on different levels of netsting

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 12:07):

but as you prefer

view this post on Zulip Ali Caglayan (Mar 02 2022 at 12:21):

OK, i've modified the subdir generator to close when it has an exception.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:06):

Nice!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):

Now that we build the ocaml stuff with dune

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):

we could dramatically speedup things

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):

by using coqdep as an ML library

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):

and sharing the context for all test-suite files

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):

the costly part of coqdep is the -R -Q setup

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 13:08):

that filesystem scan kill everything due to the kernel context switches

view this post on Zulip Paolo Giarrusso (Mar 02 2022 at 14:55):

This might be related? https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users/topic/coqdep.208.2E15.20slowdown.2C.20and.20per-library.20coqdep

view this post on Zulip Ali Caglayan (Mar 02 2022 at 14:56):

I have a patch to package up coqdep

view this post on Zulip Ali Caglayan (Mar 02 2022 at 14:57):

https://github.com/coq/coq/pull/15764

view this post on Zulip Ali Caglayan (Mar 02 2022 at 14:58):

I was hoping to do a little sharing with the rest of the library with this, but I guess it is a start.

view this post on Zulip Ali Caglayan (Mar 02 2022 at 14:58):

Then we can rely on the coqdep library (Coqdeplib) we expose here

view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:38):

@Emilio Jesús Gallego Arias Can you rebase on top of #15764?

view this post on Zulip Ali Caglayan (Mar 02 2022 at 15:38):

Then I can start using the coqdep code

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 15:55):

Yes, one sec

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:02):

Done @Ali Caglayan

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:06):

Umm the rebase seems weird XD

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:07):

What happened?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:07):

ok fixed

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:07):

no idea, also coqdep path changed

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:08):

we should look for it in the path, but OCaml 4.05 was missing some fucntion

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:08):

that will go away once we use coqdep as a library

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:08):

That's an issue with the other PR then

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:13):

I put the executable stanza in the dune file in the coqdep folder, perhaps I should put it back in tools?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:21):

It is fine where it is IMHO

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:46):

I'm seriously confused about the META business. Where is it supposed to be? Are we just missing a rule?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):

Yes we are missing a dep in the rule likely

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):

coqc needs meta to be in place

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):

to locate plugins now

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):

but there is a legacy compat code

view this post on Zulip Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):

that should work


Last updated: Feb 05 2023 at 22:03 UTC