Michael Soegtrop (Jun 14 2021 at 09:09): Michael Soegtrop (Jun 14 2021 at 09:09):@Enrico Tassi : I get some strange inconsistent failures with HB dev in Coq Platform dev.
Enrico Tassi (Jun 14 2021 at 09:10):The one on windows could be an EOL issue
Enrico Tassi (Jun 14 2021 at 09:11):We diff with an expected output. Let me check the manpage of diff. On Ubuntu I've to dig deeper
Michael Soegtrop (Jun 14 2021 at 09:13):Perfect, thanks! I will disable HB in dev until it is fixed to get forward.
Enrico Tassi (Jun 14 2021 at 09:14):Do you know if --strip-trailing-cr is the way to make windows happy (assuming it's a \r problem, I've no experience on windows)
Enrico Tassi (Jun 14 2021 at 09:15):This is the code that fails misteriously on windows
$(COQC) $(COQFLAGS) $(COQLIBS) tests/compress_coe.v > tests/compress_coe.v.out.aux; \
diff -u tests/compress_coe.v.out tests/compress_coe.v.out.aux
This option is supported on Mac as well, so I would say yes.
Enrico Tassi (Jun 14 2021 at 09:15):ok, I'll try that
Michael Soegtrop (Jun 14 2021 at 09:16):Does mathcomp dev require HB?
Michael Soegtrop (Jun 14 2021 at 09:17):In case of a mismatch, you could cat the diff
Enrico Tassi (Jun 14 2021 at 09:18):not yet, we did not merge in master the branch using HB. (it will be called MC 2.0 then, so it won't happend overnight)
Enrico Tassi (Jun 14 2021 at 09:18):wrt the diff, I do cat it... but my eye sees no difference
Enrico Tassi (Jun 14 2021 at 09:18):I'll push the flag, it won't hurt
Michael Soegtrop (Jun 14 2021 at 09:29):OK, then I leave HB in to test it.
Michael Soegtrop (Jun 14 2021 at 13:34):It still fails - as it looks it doesn't pick up your change. See:
https://github.com/coq/platform/runs/2818744615?check_suite_focus=true#step:5:2961
I don't understand why - I definitely started it after your commit.
Michael Soegtrop (Jun 14 2021 at 13:40):Sorry likely wrong - this did run before your commit
Michael Soegtrop (Jun 14 2021 at 13:46):Ehm no, it still doesn't work. It pulled the sources 10:22 GMT and your commit was 9:53 GMT.
Michael Soegtrop (Jun 14 2021 at 13:47):I just got confused with the time zones.
Enrico Tassi (Jun 14 2021 at 13:47):I'll check the log
Michael Soegtrop (Jun 14 2021 at 13:47):Thanks!
Enrico Tassi (Jun 14 2021 at 13:47):nope
872 *) diff -u tests/compress_coe.v.out tests/compress_coe.v.out.aux ;;\
it is not my commit
Michael Soegtrop (Jun 14 2021 at 13:48):I looked at the dumped diff and also would conclude that it must be a CR issue - the log visible dumps are identical.
Enrico Tassi (Jun 14 2021 at 13:48):indeed, but my commit should add an option after -u
Michael Soegtrop (Jun 14 2021 at 13:48):Yes but why? It pulled the sources 10:22 GMT and your commit was 9:53 GMT
Michael Soegtrop (Jun 14 2021 at 13:49):Maybe there is another diff command in your scripts you overlooked?
Enrico Tassi (Jun 14 2021 at 13:49):https://github.com/math-comp/hierarchy-builder/blob/coq-master/Makefile.test-suite.coq.local
Enrico Tassi (Jun 14 2021 at 13:50):I think coq-hierarchy-builder.dev pulls from this branch (coq-master)
Enrico Tassi (Jun 14 2021 at 13:50):if not, that is the problem
Michael Soegtrop (Jun 14 2021 at 13:51):It says src: "git+https://github.com/math-comp/hierarchy-builder.git#coq-master
Enrico Tassi (Jun 14 2021 at 13:51):indeed, so I've no clue why it did not pick it up, we can just retry now
Michael Soegtrop (Jun 14 2021 at 13:52): Enrico Tassi (Jun 14 2021 at 13:52):yes, that is correct
Michael Soegtrop (Jun 14 2021 at 13:52):I don't have a local patch for that in coq platform
Enrico Tassi (Jun 14 2021 at 13:53):there is no other test/diff... so it pulled the wrong sources
Michael Soegtrop (Jun 14 2021 at 13:53):Interesting ...
Enrico Tassi (Jun 14 2021 at 13:53):are we sure about the time? maybe these VMs are misconfigured
Michael Soegtrop (Jun 14 2021 at 13:53):Too bad opam doesn't show the hashes
Enrico Tassi (Jun 14 2021 at 13:53):let's just re-run them
Michael Soegtrop (Jun 14 2021 at 13:54):Well I waited to see your commit before I started CI and the logs confirm that.
Michael Soegtrop (Jun 14 2021 at 13:54):I will try that
Michael Soegtrop (Jun 14 2021 at 13:56):Did you look into the Ubuntu thing? (https://github.com/coq/platform/pull/102/checks?check_run_id=2818744540). Possibly a file name capitalization issue (macOS is also case insensitive by default).
Enrico Tassi (Jun 14 2021 at 13:56):https://github.com/ocaml/opam/issues/3567
Enrico Tassi (Jun 14 2021 at 13:57):One thing is that we don't install the examples anymore. So maybe the smoke test is not "self contained" anymore
Enrico Tassi (Jun 14 2021 at 13:58):let me check
Michael Soegtrop (Jun 14 2021 at 13:59):Ah yes, I thought in Mac it goes beyond that since it fails in the installer, but the smoke test kit test is done after the installer on the installed version.
Michael Soegtrop (Jun 14 2021 at 14:00):So likely on macOS it will fail as well.
Enrico Tassi (Jun 14 2021 at 14:00):so yes, you should also include the required file
Enrico Tassi (Jun 14 2021 at 14:01):no, sorry, I'm wrong... it is self contained
Enrico Tassi (Jun 14 2021 at 14:02):I think it just misses a -Q (the file has a From demo2...) https://github.com/math-comp/hierarchy-builder/blob/master/examples/demo2/stage10.v#L3
Enrico Tassi (Jun 14 2021 at 14:02):I thnk you reported this problem already, but I did not fix it
Enrico Tassi (Jun 14 2021 at 14:02):let me do it now
Michael Soegtrop (Jun 14 2021 at 14:03):Possibly - I sometimes loos track ...
Michael Soegtrop (Jun 14 2021 at 14:03):For the DMG installer the plist file is gone from the Coq sources. We discussed that it is copied to Coq Platform, but I didn't do it as yet. Will do so now.
Enrico Tassi (Jun 14 2021 at 14:05):done
Enrico Tassi (Jun 14 2021 at 14:05):if you restart the build, it should be fixed (or broken for another reason)
Michael Soegtrop (Jun 14 2021 at 14:11):I am really looking forward to have a daily dev CI again, so that these things come one by one ...
Michael Soegtrop (Jun 14 2021 at 14:14):I pushed the plist fix - bets are still open ;-)
Michael Soegtrop (Jun 14 2021 at 14:18):If the Windows issues doesn't go away, I would suggest to run the result of coqc through tr -d '\r'
Michael Soegtrop (Jun 15 2021 at 12:48):@Enrico Tassi : things are getting better - the CR stuff is gone - but there are some path name forward backward slash differences now. See (https://github.com/coq/platform/pull/102/checks?check_run_id=2820631352#step:5:10180).
Enrico Tassi (Jun 15 2021 at 13:46):OK, that is the fname component of the Loc.t datatype https://github.com/coq/coq/blob/master/lib/loc.mli#L18
Enrico Tassi (Jun 15 2021 at 13:47):I can clearly fix it on the Coq-Elpi side, before printing it. But I think Coq should stop using the ocaml filename separator, and just use / on all platforms since it is just better
Enrico Tassi (Jun 15 2021 at 13:57):So, it turns out the printing of loc is done in elpi (not coq-elpi), so a commit to (elpi) master won't pick it up since there is no elpi.dev package.
It happens I'm also working on elpi for a minor fix, which may lead to a point release, but won't happen today.
I can hack it up in HB's code calling diff, as for \r, but I'm not super happy...
Enrico Tassi (Jun 15 2021 at 14:00):if you want a quick fix, I suggest you overlay hb by picking a more recent opam file (https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-hierarchy-builder/coq-hierarchy-builder.dev/opam is old). The new build process separates "build" and "test-suite" and you can just comment the second call: https://github.com/math-comp/hierarchy-builder/blob/master/coq-hierarchy-builder.opam#L12
Michael Soegtrop (Jun 15 2021 at 15:41):Thanks, I will update the opam file and comment out the test part.
Pierre Roux (Jun 15 2021 at 15:49):Maybe could it be activated only by the with-test variable https://opam.ocaml.org/doc/Manual.html#pkgvar-with-test
Enrico Tassi (Jun 15 2021 at 16:22):That was my original plan, but the docker action did not support it (yet?)
Michael Soegtrop (Jun 17 2021 at 08:04):@Enrico Tassi : I now updated the opam file for hierarchy builder (in the Coq Platform local opam patch repo) - let's see.
Should we have an elpi.dev package?
Enrico Tassi (Jun 17 2021 at 09:38):I never target elpi master, only released versions, so I would not mind.
Michael Soegtrop (Jun 17 2021 at 13:19):I tried the new HB opam package - not successful, see:
https://github.com/coq/platform/pull/102/checks?check_run_id=2846810688#step:5:2083
Can you please check if I did something silly in my branch? The opam package is here:
https://github.com/MSoegtropIMC/platform/blob/multi-version/opam/opam-coq-archive/extra-dev/packages/coq-hierarchy-builder/coq-hierarchy-builder.dev/opam
Enrico Tassi (Jun 18 2021 at 06:39):You did not comment out the make test suite, or uncomment the with-test flag.
Enrico Tassi (Jun 18 2021 at 06:40):I hope to fix the issue upstream today, anyway
Enrico Tassi (Jun 18 2021 at 06:51):The log seems to point to a remake file not being patched, 8-/
Enrico Tassi (Jun 18 2021 at 10:01):The new version of elpi, which prints / as a path separator also on windows, was merged in the main opam repo a minute ago.
As soon as the archive gets in sync, I'll release coq-elpi...
Pierre Roux (Jun 24 2021 at 14:34):@Enrico Tassi said:
That was my original plan, but the docker action did not support it (yet?)
@Erik Martin-Dorel told me it could work, I let him give the details
Enrico Tassi (Jun 24 2021 at 14:35):Erik implemented it since, I found it in the examples: https://github.com/LPCIC/coq-elpi/blob/23345e95657b71f98dd6e4cd1941764018937490/.github/workflows/main.yml#L29
Enrico Tassi (Jun 24 2021 at 14:36):thanks for the heads up anyway!
Last updated: Apr 18 2024 at 19:02 UTC