@Enrico Tassi : I get some strange inconsistent failures with HB dev in Coq Platform dev.
The one on windows could be an EOL issue
We diff with an expected output. Let me check the manpage of diff. On Ubuntu I've to dig deeper
Perfect, thanks! I will disable HB in dev until it is fixed to get forward.
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)
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.
ok, I'll try that
Does mathcomp dev require HB?
In case of a mismatch, you could cat the diff
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)
wrt the diff, I do cat it... but my eye sees no difference
I'll push the flag, it won't hurt
OK, then I leave HB in to test it.
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.
Sorry likely wrong - this did run before your commit
Ehm no, it still doesn't work. It pulled the sources 10:22 GMT and your commit was 9:53 GMT.
I just got confused with the time zones.
I'll check the log
Thanks!
nope
872 *) diff -u tests/compress_coe.v.out tests/compress_coe.v.out.aux ;;\
it is not my commit
I looked at the dumped diff and also would conclude that it must be a CR issue - the log visible dumps are identical.
indeed, but my commit should add an option after -u
Yes but why? It pulled the sources 10:22 GMT and your commit was 9:53 GMT
Maybe there is another diff command in your scripts you overlooked?
https://github.com/math-comp/hierarchy-builder/blob/coq-master/Makefile.test-suite.coq.local
I think coq-hierarchy-builder.dev pulls from this branch (coq-master)
if not, that is the problem
It says src: "git+https://github.com/math-comp/hierarchy-builder.git#coq-master
indeed, so I've no clue why it did not pick it up, we can just retry now
yes, that is correct
I don't have a local patch for that in coq platform
there is no other test/diff... so it pulled the wrong sources
Interesting ...
are we sure about the time? maybe these VMs are misconfigured
Too bad opam doesn't show the hashes
let's just re-run them
Well I waited to see your commit before I started CI and the logs confirm that.
I will try that
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).
https://github.com/ocaml/opam/issues/3567
One thing is that we don't install the examples anymore. So maybe the smoke test is not "self contained" anymore
let me check
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.
So likely on macOS it will fail as well.
so yes, you should also include the required file
no, sorry, I'm wrong... it is self contained
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
I thnk you reported this problem already, but I did not fix it
let me do it now
Possibly - I sometimes loos track ...
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.
done
if you restart the build, it should be fixed (or broken for another reason)
I am really looking forward to have a daily dev CI again, so that these things come one by one ...
I pushed the plist fix - bets are still open ;-)
If the Windows issues doesn't go away, I would suggest to run the result of coqc through tr -d '\r'
@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).
OK, that is the fname component of the Loc.t datatype https://github.com/coq/coq/blob/master/lib/loc.mli#L18
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
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...
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
Thanks, I will update the opam file and comment out the test part.
Maybe could it be activated only by the with-test variable https://opam.ocaml.org/doc/Manual.html#pkgvar-with-test
That was my original plan, but the docker action did not support it (yet?)
@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?
I never target elpi master, only released versions, so I would not mind.
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
You did not comment out the make test suite, or uncomment the with-test flag.
I hope to fix the issue upstream today, anyway
The log seems to point to a remake file not being patched, 8-/
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...
@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
Erik implemented it since, I found it in the examples: https://github.com/LPCIC/coq-elpi/blob/23345e95657b71f98dd6e4cd1941764018937490/.github/workflows/main.yml#L29
thanks for the heads up anyway!
Last updated: Oct 13 2024 at 01:02 UTC