ProofWidgets v0.0.36 and v0.0.39

Stream: general

[Kim Morrison]

@Wojciech Nawrocki, I made a bit of a mess of the releases in ProofWidgets yesterday, creating v0.0.37, v0.0.38, and v0.0.38, all of which use the (as yet unannounced) v4.8.0 toolchain, but I couldn't get Mathlib on v4.8.0 to successfully use any of them because of noisy build reports from ProofWidgets.

Hence I'm going to move Mathlib to v4.8.0 still using v0.0.36 for now (despite the toolchain mismatch), and this seems to work.

So:

1. If you want to just delete v0.0.37, v0.0.38, and v0.0.39, no objections from me, and apologies for cutting so many!
2. There underlying reason for the failures was that you have made significant changes (with Mac) to the build setup, but these had only landed on master, not in a release. Thus when I needed to release the v4.8.0 toolchain, I was trapped, because ProofWidgets master was not even compatible with being used in Mathlib at v4.8.0-rc2.
3. In future, if you make major changes to the build setup, can you please cut a new release, and either notify me that we need to do a Mathlib bump (or do it yourself, or find other Mathlib maintainers to do it). I'd really like to avoid the situation that I need a new release to do a Lean version release, but find myself with a master that hasn't actually been tested yet on downstream repos!

Can I leave it to you to work out what needs to change so ProofWidgets is compatible with Mathlib again? Currently, it will run npm install in the Mathlib build process, which inevitably fails.

[Mac Malone]

@Wojciech Nawrocki Sorry for not testing this stuff throughly and verifying it works when I was helping you with the build overhaul. Once suggestion I do have is that it would be good to have a release test in the CI. For example, something like:

lake clean && lake build :release && lake build --no-build

I have been debugging main and it is not yet clear to me why the build is broken. The main thing I have deduced is that the produced release lake.trace does not match that which is computed locally when using the release.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Mac Malone said:

The main thing I have deduced is that the produced release lake.trace does not match that which is computed locally when using the release.

I am observing that the hash of some inputFiles is platform-dependent. That shouldn't be the case, should it? See the two builds here which differ in "trace hash pre package-lock".

UPDATE: Oh lol, I think it might just be because the files are listed in an inconsistent order across platforms.

UPDATE 2: Yeah I think that was it.

UPDATE 3: Not quite, sorting equates the hash across Ubuntu and my local Mac, but not across Ubuntu and Windows.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Mac Malone : Looking at this run now, the trace of inputFiles differs between Ubuntu and Windows. Is this intended?

[Mac Malone]

@Wojciech Nawrocki Are you using inputFile itself (which is deprecated) or the new inputTextFile? The old inputFile is a binary comparison. inputTextFile normalizes line endings. On Windows, byt default, GitHub checks out text files with CRLF line endings which makes files not binary equal.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I think inputTextFile might not exist on 4.9.0-rc2? I will try rc3.

UPDATE: Nope, not there on rc3 either.

[Mac Malone]

True, However, the underlying problem is still there. So you can try copy-pasting the definition of inputTextFile from master.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Okay, that fixed the input files. It looks like buildFileAfterDep has the same issue in case the build output is checked out by git, but the .hash file is not.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Now it cannot find a file that is clearly there. Any ideas @Mac Malone ? Ok, it's not there.

[Mac Malone]

@Wojciech Nawrocki Oh yes, build artifacts are not expected to be git-managed.

[Mac Malone]

If they are, you may want to use .gitattributes to clarify the expected format (e.g., eol)