Ali Caglayan (Mar 01 2022 at 17:43): 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?
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
Emilio Jesús Gallego Arias (Mar 01 2022 at 17:53):I'm afraid not a short term other than tweaking NJOBS env var
Emilio Jesús Gallego Arias (Mar 01 2022 at 17:54):See the rule in test-suite/dune
Ali Caglayan (Mar 01 2022 at 21:55):OK tweaking NJOBS works
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):I suggest we use this thread to discuss about the test-suite PR
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):@Ali Caglayan
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):I did rebase and things seem OK except for a couple of issues
Ali Caglayan (Mar 02 2022 at 11:53):Yep my rebase looked pretty similar
Ali Caglayan (Mar 02 2022 at 11:53):The META stuff I think can be fixed by passing the correct -I right?
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):It runs fine on my computer with dune build @test-gen
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:53):then dune runtest
Ali Caglayan (Mar 02 2022 at 11:54):Does runtest not call test-gen?
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
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
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:54):But we can do a little make rule as I did here
Ali Caglayan (Mar 02 2022 at 11:54):OK so the coq-core.plugins.ltac can be fixed by changing it to ltac_plugin
Ali Caglayan (Mar 02 2022 at 11:55):But there is a syntax error from coqdep in bugs/12138
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:55): 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
Ali Caglayan (Mar 02 2022 at 11:55):So I moved it to a seperate folder where we won't call coqdep on tests
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:55):we need to fix coqdep
Ali Caglayan (Mar 02 2022 at 11:55):Fixing coqdep is tricky though because it uses . for terminals but the test has {.
Emilio Jesús Gallego Arias (Mar 02 2022 at 11:56):I see, I guess we'll figure out a compromise.
Ali Caglayan (Mar 02 2022 at 11:57):My fix for the META stuff is just a work around however
Ali Caglayan (Mar 02 2022 at 11:57):We need to pass -I correctly to coqdep for this to work
Ali Caglayan (Mar 02 2022 at 11:58):currently we are only passing ltac
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
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?
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
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):eventually we may use a dune file
Ali Caglayan (Mar 02 2022 at 12:00):Right, but should we be looking in install?
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):with (coq.theories ...)
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?
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:00):IMHO we shouldn't touch install
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
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
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?
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):if so we want to fix it, but there was some problem
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):so that's like a temporary solution I think
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
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:02):but it could involve patching dune or findlib
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):I propose we look at this last
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):as I have some fixes pending for the META stuff
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:03):so use install or whatever works best for you
Ali Caglayan (Mar 02 2022 at 12:05):There is also a small problem with the rule generation
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
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
Ali Caglayan (Mar 02 2022 at 12:06):I have to keep fixing it with a closing paranthesis
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):yes, that's a pain, I have to do rm + touch
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):indeed I propose we add to gen_rules a clean setp
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):that truncates the file if an exception
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:06):or your fav workaround
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:07):I'm going for lunch, the tree is fully yours
Ali Caglayan (Mar 02 2022 at 12:07):Is it too hacky to just add a brace at the end?
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
Emilio Jesús Gallego Arias (Mar 02 2022 at 12:07):but as you prefer
Ali Caglayan (Mar 02 2022 at 12:21):OK, i've modified the subdir generator to close when it has an exception.
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:06):Nice!
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):Now that we build the ocaml stuff with dune
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):we could dramatically speedup things
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):by using coqdep as an ML library
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):and sharing the context for all test-suite files
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:07):the costly part of coqdep is the -R -Q setup
Emilio Jesús Gallego Arias (Mar 02 2022 at 13:08):that filesystem scan kill everything due to the kernel context switches
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
Ali Caglayan (Mar 02 2022 at 14:56):I have a patch to package up coqdep
Ali Caglayan (Mar 02 2022 at 14:57):https://github.com/coq/coq/pull/15764
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.
Ali Caglayan (Mar 02 2022 at 14:58):Then we can rely on the coqdep library (Coqdeplib) we expose here
Ali Caglayan (Mar 02 2022 at 15:38):@Emilio Jesús Gallego Arias Can you rebase on top of #15764?
Ali Caglayan (Mar 02 2022 at 15:38):Then I can start using the coqdep code
Emilio Jesús Gallego Arias (Mar 02 2022 at 15:55):Yes, one sec
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:02):Done @Ali Caglayan
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:06):Umm the rebase seems weird XD
Ali Caglayan (Mar 02 2022 at 16:07):What happened?
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:07):ok fixed
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:07):no idea, also coqdep path changed
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
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:08):that will go away once we use coqdep as a library
Ali Caglayan (Mar 02 2022 at 16:08):That's an issue with the other PR then
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?
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:21):It is fine where it is IMHO
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?
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):Yes we are missing a dep in the rule likely
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):coqc needs meta to be in place
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):to locate plugins now
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):but there is a legacy compat code
Emilio Jesús Gallego Arias (Mar 02 2022 at 16:47):that should work
Last updated: Dec 07 2023 at 14:02 UTC