Stream: Coq devs & plugin devs

Topic: ✔ How to pass jobs to test-suite build


view this post on Zulip Ali Caglayan (Aug 09 2021 at 17:06):

Nice, NJOBS worked

view this post on Zulip Notification Bot (Aug 09 2021 at 17:07):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Aug 09 2021 at 19:16):

@Gaëtan Gilbert <s>Acutally, I haven't got your branch to work</s> Nevermind I am being silly

view this post on Zulip Emilio Jesús Gallego Arias (Aug 11 2021 at 19:37):

Gaëtan Gilbert said:

merge https://github.com/coq/coq/pull/14625, then stop using Makefile.dune for the test suite

Actually I don't follow why we want people not to do the test-suite from dune

view this post on Zulip Emilio Jesús Gallego Arias (Aug 11 2021 at 19:38):

what is the problem? has been running fine for a long time, and moreover it is hygienic

view this post on Zulip Gaëtan Gilbert (Aug 11 2021 at 19:39):

because being able to run subsets of it is important, and running through dune means the logs end up in _build and get cleaned if you run another dune command

view this post on Zulip Emilio Jesús Gallego Arias (Aug 11 2021 at 19:40):

Ok, thanks, I guess we should move forward with the port

view this post on Zulip Théo Zimmermann (Aug 11 2021 at 22:25):

Absolutely! I look forward to the Dune port. But until then, I will indeed prefer the non-hygienic, but more incremental test-suite build.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 12 2021 at 12:30):

Tho we could play some trick with promote + allowing a subtarget as to fix this


Last updated: Oct 16 2021 at 02:03 UTC