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?
I know there is a wip port of the test-suite to dune, but I am looking for short term solutions
I'm afraid not a short term other than tweaking NJOBS env var
See the rule in test-suite/dune
OK tweaking NJOBS works
I suggest we use this thread to discuss about the test-suite PR
@Ali Caglayan
I did rebase and things seem OK except for a couple of issues
Yep my rebase looked pretty similar
The META stuff I think can be fixed by passing the correct -I right?
It runs fine on my computer with dune build @test-gen
then dune runtest
Does runtest not call test-gen?
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
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
But we can do a little make rule as I did here
OK so the coq-core.plugins.ltac can be fixed by changing it to ltac_plugin
But there is a syntax error from coqdep in bugs/12138
Ali Caglayan said:
But there is a syntax error from coqdep in bugs/12138
Yes, I did remove it for now
So I moved it to a seperate folder where we won't call coqdep on tests
we need to fix coqdep
Fixing coqdep is tricky though because it uses .
for terminals but the test has {
.
I see, I guess we'll figure out a compromise.
My fix for the META stuff is just a work around however
We need to pass -I correctly to coqdep for this to work
currently we are only passing ltac
I wanted to maybe copy what is being done in the shims but I don't really understand that
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?
@Ali Caglayan this is hardcoded for now, but it doesn't look wrong to me
eventually we may use a dune
file
Right, but should we be looking in install?
with (coq.theories ...)
Ali Caglayan said:
Right, but should we be looking in install?
what do you mean?
IMHO we shouldn't touch install
(bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop} -I \"$(dirname \"$0\")/%{project_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")/%{project_root}\" \"$@\"'")
this is from the shim
unless we want to add a flag for running the test suite vs an installed Coq, but I don't see the use case
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?
if so we want to fix it, but there was some problem
so that's like a temporary solution I think
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
but it could involve patching dune or findlib
I propose we look at this last
as I have some fixes pending for the META stuff
so use install or whatever works best for you
There is also a small problem with the rule generation
Ali Caglayan said:
There is also a small problem with the rule generation
tell me
If there is an excpetion, such as the ones we currently get, we get an unbalanced sexp
I have to keep fixing it with a closing paranthesis
yes, that's a pain, I have to do rm + touch
indeed I propose we add to gen_rules a clean setp
that truncates the file if an exception
or your fav workaround
I'm going for lunch, the tree is fully yours
Is it too hacky to just add a brace at the end?
I would just truncate the file on the exception handler, seems simpler, as we may be on different levels of netsting
but as you prefer
OK, i've modified the subdir generator to close when it has an exception.
Nice!
Now that we build the ocaml stuff with dune
we could dramatically speedup things
by using coqdep as an ML library
and sharing the context for all test-suite files
the costly part of coqdep is the -R -Q setup
that filesystem scan kill everything due to the kernel context switches
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
I have a patch to package up coqdep
https://github.com/coq/coq/pull/15764
I was hoping to do a little sharing with the rest of the library with this, but I guess it is a start.
Then we can rely on the coqdep library (Coqdeplib) we expose here
@Emilio Jesús Gallego Arias Can you rebase on top of #15764?
Then I can start using the coqdep code
Yes, one sec
Done @Ali Caglayan
Umm the rebase seems weird XD
What happened?
ok fixed
no idea, also coqdep path changed
we should look for it in the path, but OCaml 4.05 was missing some fucntion
that will go away once we use coqdep as a library
That's an issue with the other PR then
I put the executable stanza in the dune file in the coqdep folder, perhaps I should put it back in tools?
It is fine where it is IMHO
I'm seriously confused about the META business. Where is it supposed to be? Are we just missing a rule?
Yes we are missing a dep in the rule likely
coqc needs meta to be in place
to locate plugins now
but there is a legacy compat code
that should work
Last updated: Jun 08 2023 at 04:01 UTC