ProofWidgets bump required

Stream: mathlib4

[Scott Morrison]

Merging @Patrick Massot's std4#267 means that we can't update Mathlib to Std main until ProofWidgets has been updated. (Otherwise we end up with two copies of the json% macro, and you can't import both.)

I've made the necessary ProofWidgets PR at https://github.com/leanprover-community/ProofWidgets4/pull/28

What I don't know how to do is create a ProofWidgets release. @Wojciech Nawrocki @Gabriel Ebner, would either of you be able to tell me how to do this?

[Scott Morrison]

I think it is as simple as:

• merge the PR
• create and push the tag v0.0.19
• run lake upload v0.0.19

but would be happy to have confirmation. :-)

[Scott Morrison]

That can't be quite right, as nothing in that process will create the release. Presumably I do this via https://github.com/leanprover-community/ProofWidgets4/releases/new

[Wojciech Nawrocki]

@Scott Morrison that's almost it: create the release first, then upload the archive. Except that you also need to push archives for other platforms, otherwise builds on non-MacOS will fail. The manual process I had been using is to simply upload the same archive with different names: the JS files are the same, and it's fine if the .oleans are rebuilt. But maybe it's high time to have CI do this for us: let me try to set that up.

[Scott Morrison]

Amazing. :-)

[Scott Morrison]

I was just booting up my virtual linux box. Nice to know the files are all the same. :-)

[Wojciech Nawrocki]

@Scott Morrison should happen automatically now, just make a new release (or push a new tag from the CLI) and wait a bit.

[Scott Morrison]

@Wojciech Nawrocki, lean4checker is failing on the bump PRs that move to ProofWidgets v0.0.19, with the error

lean4checker found a problem in «._ProofWidgets»
uncaught exception: unknown package '«._ProofWidgets»'

Presumably some piece of code is doing an open ._ProofWidgets somehow, and failing. Do you have any guesses where this could be coming from?

[Scott Morrison]

Oooh! @Mac Malone could this be the lakefile.olean for ProofWidgets, being included in the release bundle?

That would explain why it is only showing up now.

[Scott Morrison]

For now I am just going to have lean4checker ignore this specifically. But this is a hack! @Mac Malone, if you are able to tell me whether

• I'm wrong about this being the lakefile.olean
• You'll plan to make sure it isn't delivered with the release bundle
• lean4checker should assume that it has to deal with these files, in which case it would be nice to know what the module names will be

that would be great

[Mario Carneiro]

I think it is due to a bunch of ._foo files in the tar.gz (MacOS directory junk?)

[Scott Morrison]

Wojciech Nawrocki said:

Scott Morrison should happen automatically now, just make a new release (or push a new tag from the CLI) and wait a bit.

@Wojciech Nawrocki, the v0.0.20 release doesn't appear to have a macOS-64.tar.gz

[Scott Morrison]

@Mario Carneiro where are you seeing these files? I'm not finding them.

[Mario Carneiro]

they are in https://github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.19/linux-64.tar.gz

[Mario Carneiro]

if you are on macos you might have to set some settings to see them since these are hidden files

[Mario Carneiro]

after unpacking:

$ ls -al lib
total 68
drwxr-xr-x 3 mario mario  4096 Oct 23 20:37 .
drwxrwxr-x 5 mario mario  4096 Oct 24 01:44 ..
-rwxr-xr-x 1 mario mario   163 Oct 23 20:36 ._ProofWidgets
drwxr-xr-x 5 mario mario  4096 Oct 23 20:36 ProofWidgets
-rw-r--r-- 1 mario mario   163 Oct 23 20:37 ._ProofWidgets.ilean
-rw-r--r-- 1 mario mario    53 Oct 23 20:37 ProofWidgets.ilean
-rw-r--r-- 1 mario mario   163 Oct 23 20:37 ._ProofWidgets.ilean.hash
-rw-r--r-- 1 mario mario    19 Oct 23 20:37 ProofWidgets.ilean.hash
-rw-r--r-- 1 mario mario   163 Oct 23 20:37 ._ProofWidgets.olean
-rw-r--r-- 1 mario mario 12688 Oct 23 20:37 ProofWidgets.olean
-rw-r--r-- 1 mario mario   163 Oct 23 20:37 ._ProofWidgets.olean.hash
-rw-r--r-- 1 mario mario    20 Oct 23 20:37 ProofWidgets.olean.hash
-rw-r--r-- 1 mario mario   163 Oct 23 20:37 ._ProofWidgets.trace
-rw-r--r-- 1 mario mario    20 Oct 23 20:37 ProofWidgets.trace

[Scott Morrison]

% ls -al
total 64
drwxr-xr-x@  8 kim  staff    256 Oct 24 11:37 .
drwx------@  5 kim  staff    160 Oct 24 16:43 ..
drwxr-xr-x@ 10 kim  staff    320 Oct 24 11:36 ProofWidgets
-rw-r--r--@  1 kim  staff     53 Oct 24 11:37 ProofWidgets.ilean
-rw-r--r--@  1 kim  staff     19 Oct 24 11:37 ProofWidgets.ilean.hash
-rw-r--r--@  1 kim  staff  12688 Oct 24 11:37 ProofWidgets.olean
-rw-r--r--@  1 kim  staff     20 Oct 24 11:37 ProofWidgets.olean.hash
-rw-r--r--@  1 kim  staff     20 Oct 24 11:37 ProofWidgets.trace

[Scott Morrison]

Are you on a mac? Could my system be intercepting them as it unzips??

[Mario Carneiro]

no, linux

[Scott Morrison]

Weird

[Scott Morrison]

What is in those files?

[Mario Carneiro]

$ xxd lib/._ProofWidgets.olean
00000000: 0005 1607 0002 0000 4d61 6320 4f53 2058  ........Mac OS X
00000010: 2020 2020 2020 2020 0002 0000 0009 0000          ........
00000020: 0032 0000 0071 0000 0002 0000 00a3 0000  .2...q..........
00000030: 0000 0000 0000 0000 0000 0000 0000 0000  ................
00000040: 0000 0000 0000 0000 0000 0000 0000 0000  ................
00000050: 0000 0000 4154 5452 0000 0000 0000 00a3  ....ATTR........
00000060: 0000 0098 0000 000b 0000 0000 0000 0000  ................
00000070: 0000 0000 0000 0001 0000 0098 0000 000b  ................
00000080: 0000 1563 6f6d 2e61 7070 6c65 2e70 726f  ...com.apple.pro
00000090: 7665 6e61 6e63 6500 0100 0073 d8f1 f187  venance....s....
000000a0: d3ec 49                                  ..I

[Mario Carneiro]

https://apple.stackexchange.com/questions/14980/why-are-dot-underscore-files-created-and-how-can-i-avoid-them

[Scott Morrison]

Yeah, just found the same one. That's ... disgusting.

[Scott Morrison]

I guess we need to have lake upload carefully avoid creating these...

[Mario Carneiro]

was that how you created this release?

[Mario Carneiro]

IIUC the proofwidgets release is a bit funny because it is "cross-platform by fiat"

[Scott Morrison]

Yes, unique amongst all ProofWidgets releases, v.0.0.19 was made on a mac!

[Mario Carneiro]

oh another tidbit: ._ files are not created on apple filesystems like HPS+ or APFS because these filesystems have a place for the resource fork data

[Mario Carneiro]

they are used for "interchange" with other filesystems

[Scott Morrison]

lean4#2742

[Scott Morrison]

I think rather than leave a gap in lean4checker's defenses here, I am going to download these files on a non-mac system, strip out this crap, and upload them again. This is so gross.

[Mario Carneiro]

How about using lean4#2743 to do that, as a test?

[Wojciech Nawrocki]

Hi, so lean4#2743 won't help here because we manually run tar rather than using lake upload due to lean4#2713. But I can adjust the CI script.

[Wojciech Nawrocki]

Scott Morrison said:

Wojciech Nawrocki said:

Scott Morrison should happen automatically now, just make a new release (or push a new tag from the CLI) and wait a bit.

Wojciech Nawrocki, the v0.0.20 release doesn't appear to have a macOS-64.tar.gz

It seems the macOS job deadlocks nondeterministically :(

[Wojciech Nawrocki]

Hopefully fixed with 0.0.21.