Stream: Hierarchy Builder devs & users

Topic: HB dev fails in Coq Platform


view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:09):

@Enrico Tassi : I get some strange inconsistent failures with HB dev in Coq Platform dev.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 09:10):

The one on windows could be an EOL issue

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:13):

Perfect, thanks! I will disable HB in dev until it is fixed to get forward.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:15):

This option is supported on Mac as well, so I would say yes.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 09:15):

ok, I'll try that

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:16):

Does mathcomp dev require HB?

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:17):

In case of a mismatch, you could cat the diff

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Jun 14 2021 at 09:18):

wrt the diff, I do cat it... but my eye sees no difference

view this post on Zulip Enrico Tassi (Jun 14 2021 at 09:18):

I'll push the flag, it won't hurt

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 09:29):

OK, then I leave HB in to test it.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:40):

Sorry likely wrong - this did run before your commit

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:47):

I just got confused with the time zones.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:47):

I'll check the log

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:47):

Thanks!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:48):

indeed, but my commit should add an option after -u

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:49):

Maybe there is another diff command in your scripts you overlooked?

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:49):

https://github.com/math-comp/hierarchy-builder/blob/coq-master/Makefile.test-suite.coq.local

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:50):

I think coq-hierarchy-builder.dev pulls from this branch (coq-master)

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:50):

if not, that is the problem

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:51):

It says src: "git+https://github.com/math-comp/hierarchy-builder.git#coq-master

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:52):

See (https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-hierarchy-builder/coq-hierarchy-builder.dev/opam)

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:52):

yes, that is correct

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:52):

I don't have a local patch for that in coq platform

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:53):

there is no other test/diff... so it pulled the wrong sources

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:53):

Interesting ...

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:53):

are we sure about the time? maybe these VMs are misconfigured

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:53):

Too bad opam doesn't show the hashes

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:53):

let's just re-run them

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:54):

Well I waited to see your commit before I started CI and the logs confirm that.

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:54):

I will try that

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:56):

https://github.com/ocaml/opam/issues/3567

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:58):

let me check

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 14:00):

So likely on macOS it will fail as well.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:00):

so yes, you should also include the required file

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:01):

no, sorry, I'm wrong... it is self contained

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:02):

I thnk you reported this problem already, but I did not fix it

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:02):

let me do it now

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 14:03):

Possibly - I sometimes loos track ...

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:05):

done

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:05):

if you restart the build, it should be fixed (or broken for another reason)

view this post on Zulip 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 ...

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 14:14):

I pushed the plist fix - bets are still open ;-)

view this post on Zulip 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'

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 15 2021 at 15:41):

Thanks, I will update the opam file and comment out the test part.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 15 2021 at 16:22):

That was my original plan, but the docker action did not support it (yet?)

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jun 17 2021 at 09:38):

I never target elpi master, only released versions, so I would not mind.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 18 2021 at 06:39):

You did not comment out the make test suite, or uncomment the with-test flag.

view this post on Zulip Enrico Tassi (Jun 18 2021 at 06:40):

I hope to fix the issue upstream today, anyway

view this post on Zulip Enrico Tassi (Jun 18 2021 at 06:51):

The log seems to point to a remake file not being patched, 8-/

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 24 2021 at 14:36):

thanks for the heads up anyway!


Last updated: Jan 29 2023 at 15:02 UTC