blueprint

Stream: FLT-regular

[Johan Commelin]

@Chris Birkbeck Can the blueprint already be viewed online somewhere?

[Yaël Dillies]

Should we have some dashboard with all the big projects happening where we can quickly access the dashboard and see what's needed?

[Alex J. Best]

Johan Commelin said:

Chris Birkbeck Can the blueprint already be viewed online somewhere?

In theory it should show up at https://leanprover-community.github.io/flt-regular/index.html but I would guess someone with access to https://github.com/leanprover-community/flt-regular/settings would have to enable pages first?

[Adam Topaz]

@Alex J. Best I think that would just display the README.md file via some jekyll template.

[Adam Topaz]

And that readme file doesn't have much in it.

[Adam Topaz]

Oh, nevermind, I see the gh-pages branch

[Adam Topaz]

I can enable pages on that branch

[Adam Topaz]

Working! https://leanprover-community.github.io/flt-regular/

[Johan Commelin]

Awesome!

[Johan Commelin]

Yaël Dillies said:

Should we have some dashboard with all the big projects happening where we can quickly access the dashboard and see what's needed?

Do you mean an enhancement of https://leanprover-community.github.io/lean_projects.html

[Yaël Dillies]

Not really, but kind of? The page you link to is about past and present projects. I want only the present ones.

[Chris Birkbeck]

Oh sorry I was afk. I see my workflow run worked! and someone enabled the page, thank you!

[Chris Birkbeck]

Ok, so now we can edit that tex file and start making it a proper blueprint. At the moment it just has some stuff from my ANT course on proving what the ring of integers is and a rough outline of the proof (following Washington's book)

[Chris Birkbeck]

I can't seem to get the links to LEAN to work with the blueprint. Does anyone know how to fix this?

[Riccardo Brasca]

The expert here is @Patrick Massot

[Eric Rodriguez]

If people want to try Alectryon for the blueprint it seems Clément has spent some time wrapping up some of the stuff I did and its now in master... Could be worth a shot :shrug:

[Chris Birkbeck]

I hadn't heard of this. Are the any guides/instructions on how to set it up?

[Chris Birkbeck]

Ah nvm, I found https://github.com/cpitclaudel/alectryon, which I guess has what I need to try it out.

[Eric Rodriguez]

I'll be making a blog post about it soon!

[Chris Birkbeck]

Ah great, that would be useful. One thing that wasn't clear from the link was if there would be any way to generate a dependency graph for/from this. Is this something one can do with this system?

[Eric Rodriguez]

No, this is basically writing a nicely formatted rich text doc from the lean - and some other nice formatting stuff but that requires some python work

[Alex J. Best]

Chris Birkbeck said:

I can't seem to get the links to LEAN to work with the blueprint. Does anyone know how to fix this?

I got it to work after a lot of attempts, we needed to have the github url and project root set in the tex src, and I had to simplify the action to not clone the repo twice.
What should the role of blueprint.tex vs web.tex be? They are basically the same at the moment and confused me a bit, do we only need one?

[Alex J. Best]

And I had to namespace some duplicated work right now, but I'm sure we can clean that up soon.

[Johan Commelin]

The difference between blueprint.tex and web.tex is that one is responsible for the PDF output, the other for the web output. You might want to do slightly different stylistic tweaks in both.

[Alex J. Best]

It seemed that changing blueprint was the only thing that worked to fix the issues though, so maybe it isn't currently set up like that. In any case we should factor out the common content right?

[Chris Birkbeck]

Thats great thank you!

[Chris Birkbeck]

Yes we should have a content.tex file and update the others from there. I hadn't done that from the start as I didnt know how different the web and blueprint needed to be

[Johan Commelin]

I can't click on nodes in the dependency graph. Is something broken?

[Johan Commelin]

(Also, it's not a connected graph, atm.)

[Alex J. Best]

It never worked, I've been trying to fix it incrementally but for a while the project wasn't building at all so it was hard to experiment

[Alex J. Best]

I'll rerun the action now

[Alex J. Best]

Ok you can now click them, but it remains totally disconnected for some reason xD

[Johan Commelin]

totally disconnected??? That's pretty bad. :rofl:

[Johan Commelin]

Hmm, I see it. The previous version was graphier.

[Alex J. Best]

I probably messed things up by changing the labels so that clicking would work

[Chris Birkbeck]

Johan Commelin said:

I can't click on nodes in the dependency graph. Is something broken?

Ah I didn't know it was meant to be clickable, it was connected originally...I can also have a look a the labels tomorrow if its still not working

[Alex J. Best]

Yeah I broke the connections when I enabled the clicking but I don't understand how still

[Chris Birkbeck]

How did you make clicking work? did the labels need to be "all_one_word"?

[Alex J. Best]

Yes exactly, the labels get turned into html IDs which don't play nice if they have spaces in, see https://github.com/PatrickMassot/leanblueprint/pull/1

[Alex J. Best]

I fixed it? But unfortunately I have no idea how, or what was broken https://leanprover-community.github.io/flt-regular/dep_graph.html looks like it now works for me at least

[Chris Birkbeck]

Oh great! It's working for me too :)

[Chris Birkbeck]

We should talk about the strategy of proof. At the moment the way I have things written one uses facts about discriminants of number fields and rings of integers to prove what the ring of integers is for a cyclotomic field. This uses, for example, embeddings of number fields into the complex numbers, which I'm not sure we currently have in mathlib (I could be wrong). I don't know of other proofs of this, so maybe there is a way to avoid all of this? or maybe we'll have to set this up as well?

[Chris Birkbeck]

That said, the statement that "An algebraic integer all of whose conjugates have absolute value one is a root of unity." would also maybe use embeddings. And I don't know a proof of flt_regular that at some point doesn't use something like this.

[Riccardo Brasca]

I agree we will need the discriminant. This is a nice subproject that is already very interesting.

[Chris Birkbeck]

Yes having something about discriminants would be good. I just don't know what to do when the proofs use something about embeddings.

[Riccardo Brasca]

Sure, we'll have to think about these proofs. But as usual we have to start with the definition...

[Chris Birkbeck]

True :)

[Riccardo Brasca]

Let's continue here

[Riccardo Brasca]

@Chris Birkbeck When you have time can you update the blueprint adding references to the Lean code? I don't remember how to do it, but it was very easy for the LTE

[Chris Birkbeck]

Ah sure! I try and do that now

[Riccardo Brasca]

A lot of results in the section "Discriminants of number fields" are now there

[Chris Birkbeck]

Ok I think its just that some of the names were outdated. I'll wait for it to build to see if its working now before adding more refs to the lean code

[Patrick Massot]

I just pushed a rather disruptive commit to the leanblueprint repo in order to enable having projects with several dependency graphs (one per chapter or section or whatever). I hope this won't break existing projects but you should keep an eye on your blueprint.

[Riccardo Brasca]

Thanks for the warning!
@Chris Birkbeck

[Chris Birkbeck]

Yes thank you! I'll keep an eye out :)

[Chris Birkbeck]

Is it just me or is the blueprint not displaying correctly? The icons for lean code etc are all huge on the page for me

[Riccardo Brasca]

Mmm yes, it's the same for me

[Chris Birkbeck]

Hmm weird. I thought it was working fine last time I made changes. I'll have a look

[Riccardo Brasca]

Also the automatic upgrade of mathlib is broken

[Riccardo Brasca]

I am doing it manually from time to time (it's not very important, it takes like 20 seconds)

[Chris Birkbeck]

@Patrick Massot Do you know why the blueprint would be rendering with huge icons? link: https://leanprover-community.github.io/flt-regular/

[Patrick Massot]

Something went really bad there. It seems you've overwritten a CSS file with a HTML file.

[Patrick Massot]

at view-source:https://leanprover-community.github.io/flt-regular/styles/theme-white.css

[Patrick Massot]

Oh actually, it's simply the default GitHub 404 page.

[Patrick Massot]

So you simply don't have that CSS file where it should be.

[Chris Birkbeck]

Yeah it got deleted somehow. Maybe if I add it back it'll work?

[Chris Birkbeck]

Ok its working now! It seem some files got deleted when @Riccardo Brasca did the bump

[Chris Birkbeck]

Thanks for the help!

[Riccardo Brasca]

I am just doing leanproject up && git commit -am "bump" && git push, I don't know why this is breaking something...

[Chris Birkbeck]

It happened here: https://github.com/leanprover-community/flt-regular/commit/6d01f711b2678c82c7261ab3db88b65ee4264e46 on Jan 2nd

[Riccardo Brasca]

Strange

[Riccardo Brasca]

The blueprint is broken again :sad:
This time my commits look normal... @Chris Birkbeck do you have an idea on what happened?

[Chris Birkbeck]

Hmm for some reason f7719b6568176bb94af3ed5e9e53799420ff1775 erased the files again. I dont quite know why this keeps happening

[Chris Birkbeck]

you can see this on the gh-pages branch

[Chris Birkbeck]

Its as if one of our actions is breaking this

[Riccardo Brasca]

https://github.com/leanprover-community/flt-regular/commit/f7719b6568176bb94af3ed5e9e53799420ff1775 looks normal

[Chris Birkbeck]

https://github.com/leanprover-community/flt-regular/commit/9edb4a36b337bcf0a79b36b987fa1d437ee77dca

[Chris Birkbeck]

sorry maybe I had the wrong one

[Riccardo Brasca]

I mean, my commits to master look normal. This one is generated by a script, right?

[Chris Birkbeck]

Yeah exactly, its one of the actions not running properly

[Chris Birkbeck]

maybe I'll just disable that bit of the action for now and then fix it. Its not like much is changing on the blueprint at the moment

[Chris Birkbeck]

although I do plan on adding stuff for case II in the not too distant future

[Riccardo Brasca]

The blueprint page is now giving an error 404. I am bumping mathlib, let's see what happens.

[Riccardo Brasca]

@Chris Birkbeck it happened again...

[Chris Birkbeck]

damn! Let me look at it again.

[Riccardo Brasca]

I've just bumped mathlib. Let's see what happens.

[Johan Commelin]

@Chris Birkbeck Can the blueprint already be viewed online somewhere?

[Yaël Dillies]

Should we have some dashboard with all the big projects happening where we can quickly access the dashboard and see what's needed?

[Alex J. Best]

Johan Commelin said:

Chris Birkbeck Can the blueprint already be viewed online somewhere?

In theory it should show up at https://leanprover-community.github.io/flt-regular/index.html but I would guess someone with access to https://github.com/leanprover-community/flt-regular/settings would have to enable pages first?

[Adam Topaz]

@Alex J. Best I think that would just display the README.md file via some jekyll template.

[Adam Topaz]

And that readme file doesn't have much in it.

[Adam Topaz]

Oh, nevermind, I see the gh-pages branch

[Adam Topaz]

I can enable pages on that branch

[Adam Topaz]

Working! https://leanprover-community.github.io/flt-regular/

[Johan Commelin]

Awesome!

[Johan Commelin]

Yaël Dillies said:

Should we have some dashboard with all the big projects happening where we can quickly access the dashboard and see what's needed?

Do you mean an enhancement of https://leanprover-community.github.io/lean_projects.html

[Yaël Dillies]

Not really, but kind of? The page you link to is about past and present projects. I want only the present ones.

[Chris Birkbeck]

Oh sorry I was afk. I see my workflow run worked! and someone enabled the page, thank you!

[Chris Birkbeck]

Ok, so now we can edit that tex file and start making it a proper blueprint. At the moment it just has some stuff from my ANT course on proving what the ring of integers is and a rough outline of the proof (following Washington's book)

[Chris Birkbeck]

I can't seem to get the links to LEAN to work with the blueprint. Does anyone know how to fix this?

[Riccardo Brasca]

The expert here is @Patrick Massot

[Eric Rodriguez]

If people want to try Alectryon for the blueprint it seems Clément has spent some time wrapping up some of the stuff I did and its now in master... Could be worth a shot :shrug:

[Chris Birkbeck]

I hadn't heard of this. Are the any guides/instructions on how to set it up?

[Chris Birkbeck]

Ah nvm, I found https://github.com/cpitclaudel/alectryon, which I guess has what I need to try it out.

[Eric Rodriguez]

I'll be making a blog post about it soon!

[Chris Birkbeck]

Ah great, that would be useful. One thing that wasn't clear from the link was if there would be any way to generate a dependency graph for/from this. Is this something one can do with this system?

[Eric Rodriguez]

No, this is basically writing a nicely formatted rich text doc from the lean - and some other nice formatting stuff but that requires some python work

[Alex J. Best]

Chris Birkbeck said:

I can't seem to get the links to LEAN to work with the blueprint. Does anyone know how to fix this?

I got it to work after a lot of attempts, we needed to have the github url and project root set in the tex src, and I had to simplify the action to not clone the repo twice.
What should the role of blueprint.tex vs web.tex be? They are basically the same at the moment and confused me a bit, do we only need one?

[Alex J. Best]

And I had to namespace some duplicated work right now, but I'm sure we can clean that up soon.

[Johan Commelin]

The difference between blueprint.tex and web.tex is that one is responsible for the PDF output, the other for the web output. You might want to do slightly different stylistic tweaks in both.

[Alex J. Best]

It seemed that changing blueprint was the only thing that worked to fix the issues though, so maybe it isn't currently set up like that. In any case we should factor out the common content right?

[Chris Birkbeck]

Thats great thank you!

[Chris Birkbeck]

Yes we should have a content.tex file and update the others from there. I hadn't done that from the start as I didnt know how different the web and blueprint needed to be

[Johan Commelin]

I can't click on nodes in the dependency graph. Is something broken?

[Johan Commelin]

(Also, it's not a connected graph, atm.)

[Alex J. Best]

It never worked, I've been trying to fix it incrementally but for a while the project wasn't building at all so it was hard to experiment

[Alex J. Best]

I'll rerun the action now

[Alex J. Best]

Ok you can now click them, but it remains totally disconnected for some reason xD

[Johan Commelin]

totally disconnected??? That's pretty bad. :rofl:

[Johan Commelin]

Hmm, I see it. The previous version was graphier.

[Alex J. Best]

I probably messed things up by changing the labels so that clicking would work

[Chris Birkbeck]

Johan Commelin said:

I can't click on nodes in the dependency graph. Is something broken?

Ah I didn't know it was meant to be clickable, it was connected originally...I can also have a look a the labels tomorrow if its still not working

[Alex J. Best]

Yeah I broke the connections when I enabled the clicking but I don't understand how still

[Chris Birkbeck]

How did you make clicking work? did the labels need to be "all_one_word"?

[Alex J. Best]

Yes exactly, the labels get turned into html IDs which don't play nice if they have spaces in, see https://github.com/PatrickMassot/leanblueprint/pull/1

[Alex J. Best]

I fixed it? But unfortunately I have no idea how, or what was broken https://leanprover-community.github.io/flt-regular/dep_graph.html looks like it now works for me at least

[Chris Birkbeck]

Oh great! It's working for me too :)

[Chris Birkbeck]

We should talk about the strategy of proof. At the moment the way I have things written one uses facts about discriminants of number fields and rings of integers to prove what the ring of integers is for a cyclotomic field. This uses, for example, embeddings of number fields into the complex numbers, which I'm not sure we currently have in mathlib (I could be wrong). I don't know of other proofs of this, so maybe there is a way to avoid all of this? or maybe we'll have to set this up as well?

[Chris Birkbeck]

That said, the statement that "An algebraic integer all of whose conjugates have absolute value one is a root of unity." would also maybe use embeddings. And I don't know a proof of flt_regular that at some point doesn't use something like this.

[Riccardo Brasca]

I agree we will need the discriminant. This is a nice subproject that is already very interesting.

[Chris Birkbeck]

Yes having something about discriminants would be good. I just don't know what to do when the proofs use something about embeddings.

[Riccardo Brasca]

Sure, we'll have to think about these proofs. But as usual we have to start with the definition...

[Chris Birkbeck]

True :)

[Riccardo Brasca]

Let's continue here

[Riccardo Brasca]

@Chris Birkbeck When you have time can you update the blueprint adding references to the Lean code? I don't remember how to do it, but it was very easy for the LTE

[Chris Birkbeck]

Ah sure! I try and do that now

[Riccardo Brasca]

A lot of results in the section "Discriminants of number fields" are now there

[Chris Birkbeck]

Ok I think its just that some of the names were outdated. I'll wait for it to build to see if its working now before adding more refs to the lean code

[Patrick Massot]

I just pushed a rather disruptive commit to the leanblueprint repo in order to enable having projects with several dependency graphs (one per chapter or section or whatever). I hope this won't break existing projects but you should keep an eye on your blueprint.

[Riccardo Brasca]

Thanks for the warning!
@Chris Birkbeck

[Chris Birkbeck]

Yes thank you! I'll keep an eye out :)

[Chris Birkbeck]

Is it just me or is the blueprint not displaying correctly? The icons for lean code etc are all huge on the page for me

[Riccardo Brasca]

Mmm yes, it's the same for me

[Chris Birkbeck]

Hmm weird. I thought it was working fine last time I made changes. I'll have a look

[Riccardo Brasca]

Also the automatic upgrade of mathlib is broken

[Riccardo Brasca]

I am doing it manually from time to time (it's not very important, it takes like 20 seconds)

[Chris Birkbeck]

@Patrick Massot Do you know why the blueprint would be rendering with huge icons? link: https://leanprover-community.github.io/flt-regular/

[Patrick Massot]

Something went really bad there. It seems you've overwritten a CSS file with a HTML file.

[Patrick Massot]

at view-source:https://leanprover-community.github.io/flt-regular/styles/theme-white.css

[Patrick Massot]

Oh actually, it's simply the default GitHub 404 page.

[Patrick Massot]

So you simply don't have that CSS file where it should be.

[Chris Birkbeck]

Yeah it got deleted somehow. Maybe if I add it back it'll work?

[Chris Birkbeck]

Ok its working now! It seem some files got deleted when @Riccardo Brasca did the bump

[Chris Birkbeck]

Thanks for the help!

[Riccardo Brasca]

I am just doing leanproject up && git commit -am "bump" && git push, I don't know why this is breaking something...

[Chris Birkbeck]

It happened here: https://github.com/leanprover-community/flt-regular/commit/6d01f711b2678c82c7261ab3db88b65ee4264e46 on Jan 2nd

[Riccardo Brasca]

Strange

[Riccardo Brasca]

The blueprint is broken again :sad:
This time my commits look normal... @Chris Birkbeck do you have an idea on what happened?

[Chris Birkbeck]

Hmm for some reason f7719b6568176bb94af3ed5e9e53799420ff1775 erased the files again. I dont quite know why this keeps happening

[Chris Birkbeck]

you can see this on the gh-pages branch

[Chris Birkbeck]

Its as if one of our actions is breaking this

[Riccardo Brasca]

https://github.com/leanprover-community/flt-regular/commit/f7719b6568176bb94af3ed5e9e53799420ff1775 looks normal

[Chris Birkbeck]

https://github.com/leanprover-community/flt-regular/commit/9edb4a36b337bcf0a79b36b987fa1d437ee77dca

[Chris Birkbeck]

sorry maybe I had the wrong one

[Riccardo Brasca]

I mean, my commits to master look normal. This one is generated by a script, right?

[Chris Birkbeck]

Yeah exactly, its one of the actions not running properly

[Chris Birkbeck]

maybe I'll just disable that bit of the action for now and then fix it. Its not like much is changing on the blueprint at the moment

[Chris Birkbeck]

although I do plan on adding stuff for case II in the not too distant future

[Riccardo Brasca]

The blueprint page is now giving an error 404. I am bumping mathlib, let's see what happens.

[Riccardo Brasca]

@Chris Birkbeck it happened again...

[Chris Birkbeck]

damn! Let me look at it again.

[Riccardo Brasca]

I've just bumped mathlib. Let's see what happens.

[Riccardo Brasca]

@Chris Birkbeck I see you are trying to make the Lean4 version working, thanks! If you manage to do it feel free to replace master with mathlib4 (current master is already backed up in mathlib3 )

[Chris Birkbeck]

Ok I think I finally got it working! (modulo some broken links) I have a test version here. But I'll move this over to the official repo tomorrow. Then we can start sorting out some details on Kummer's lemma.

[Chris Birkbeck]

Also, some names changed which I couldn't find in the new version. In particular, I probably forgot this, but do we no longer use the result about algebraic integers whoso conjugate all have norm one are roots of unity?

[Riccardo Brasca]

Mmm, I don't know, but it is in mathlib IIRC

[Chris Birkbeck]

Ah ok, then maybe I just didn't recognize the name.

[Riccardo Brasca]

docs#NumberField.Embeddings.pow_eq_one_of_norm_eq_one

[Riccardo Brasca]

@Chris Birkbeck is the blueprint working now?

[Chris Birkbeck]

Yes I think it's almost there. I've just been typing up some details of the proof of Kummers lemma before moving it to the main repo.

[Riccardo Brasca]

OK, feel free to push whatever you want (even if it's not 100% working) to the mathlib4 branch.

[Utensil Song]

I have some minor improvements and fixes on the lean4-only-dev branch (didn't want to interrupt the lean4-only branch FLT is depending on):

• fix: "Lean" links in the dependent graph, and multiple "Lean" links for one definition/theorem, these 2 edge cases were forgot to update, now they behave the same as in the blueprint main document
• improvement: no more extra/ in url
• improvement: use /find/#doc/{leandecl} instead of /find/?pattern={leandecl}#doc, the latter sometimes has some browser jumping issues

@Chris Birkbeck I'll merge them to branch lean4-only if that's ok for you.

[Chris Birkbeck]

Yes go for it! I've only been doing Tex updates, so it should be fine :)

[Chris Birkbeck]

Thank you!

[Utensil Song]

OK, just merged. CI should pick up the changes automatically.

Locally, it's best to run the following in your repo to ensure the reinstallation of blueprint:

pip uninstall -y leanblueprint
pip install -r blueprint/requirements.txt

[Chris Birkbeck]

Ok there is now a branch called blueprint_test, made from the mathlib4 branch. It should have all the mathlib4 code as well as the blueprint code and some workflows to make the blueprint. Since I'm not the owner of the repo I don't think I can make this the new master branch? Also whomever is the owner will have to set the github pages to deploy from actions.

[Chris Birkbeck]

@Riccardo Brasca Can you merge branches?

[Riccardo Brasca]

It's hosted by leanprover-community, so I think yes.

[Chris Birkbeck]

This is what the blueprint looks like on my test repo.

[Riccardo Brasca]

LGTM. Is there something we should do in the "official" repo?

[Chris Birkbeck]

Well, I think the blueprint_test needs to become the master branch so that the new github actions will run and make the blueprint (at least I can't currently see how to make them run in the branch).

[Chris Birkbeck]

Sorry maybe I wasn't clear. My test repo is completely separate from the official repo. I just copied over the code into the blueprint_test branch in the official repo, which is what I'm proposing we make the new master branch.

[Riccardo Brasca]

Yes I understand your repo is completely separated. But you can push to master in the flt-regular repo, so we can just try.

[Riccardo Brasca]

Chris Birkbeck said:

Sorry maybe I wasn't clear. My test repo is completely separate from the official repo. I just copied over the code into the blueprint_test branch in the official repo, which is what I'm proposing we make the new master branch.

Yes, go ahead. Maybe merge the mathlib4 branch, I just bumped mathlib.

[Chris Birkbeck]

Ok let me try that.

[Chris Birkbeck]

Oh this reminds me. How does one bump mathlib now? I haven't yet had to do that.

[Riccardo Brasca]

See here.

[Ruben Van de Velde]

We're not on the evil toolchain version, are we? :)

[Riccardo Brasca]

We are on

leanprover/lean4:v4.2.0-rc4

that should be good.

[Chris Birkbeck]

Hmm when I try the update it seems to break my branch. I did the curl ... and after when I try to do lake update it says error: .\lakefile.lean:1:0: error: unknown package 'Init' error: .\lakefile.lean:2:5: error: unknown namespace 'Lake' error: .\lakefile.lean:4:0: error: unexpected identifier; expected command ...

[Riccardo Brasca]

At least, I hope I didn't messed up something during the bump.

[Riccardo Brasca]

OK, it's very possible I did messed up things.

[Chris Birkbeck]

this is on the blueprint_test branch. I don't know about the mathlib4 branch.

[Ruben Van de Velde]

Why is lakefile.olean checked in?

[Riccardo Brasca]

Mmm, I am not sure.

[Riccardo Brasca]

I guess we can just remove it.

[Riccardo Brasca]

In any case everything seems to be working for me.

[Chris Birkbeck]

hmm not for me. Weird, let me play around some more

[Riccardo Brasca]

What happens if you clone a fresh copy of the repository?

[Chris Birkbeck]

Yeah I'm going to try that. I thinks its a me problem

[Chris Birkbeck]

leanprover/lean4:v4.2.0-rc4 this seems broken for me. I can't get the mathlib4 branch to work and I also can't bump the blueprint_test branch since once I run curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain and then try to run lake update I get the error: .\lakefile.lean:1:0: error: unknown package 'Init' errors again.

[Chris Birkbeck]

@Riccardo Brasca maybe you can try bumping the blueprint_test branch to see if it works for you?

[Riccardo Brasca]

blueprint_test works for me

[Riccardo Brasca]

Let me see if I can bump it. How old is mathlib on this branch?

[Chris Birkbeck]

its leanprover/lean4:v4.2.0-rc1

[Utensil Song]

try which lake to determine the lake version you are running

[Utensil Song]

what you are experiencing has been reported on zulip before

[Utensil Song]

it's possible that the ghost of old lake causing this

[Chris Birkbeck]

ahh I see. Which lake just returns /c/Users/chris/.elan/bin/lake

[Chris Birkbeck]

Do I just need to run lake update?

[Utensil Song]

it's recommended to ensure both the removal of lakefile.olean and lake-packages first

[Utensil Song]

no, lake update will mess things up further

[Utensil Song]

what about lake -v

[Chris Birkbeck]

Lake version 5.0.0-a62d2fd (Lean version 4.2.0-rc1)

[Chris Birkbeck]

lake --version is what gave me that

[Utensil Song]

rc1 is relatively safer than rc2 and rc3

[Riccardo Brasca]

I've pushed a branch blueprint_bump merging mathlib4 into blueprint_test

[Riccardo Brasca]

I am checking that everything works there (I had a couple of conflicts that I resolved randomly)

[Riccardo Brasca]

It seems OK. Let's try to make it the master branch

[Chris Birkbeck]

Ok great!

[Riccardo Brasca]

mmm.. does anyone know how to do it? merge is of course the wrong answer here, the two branches diverged completely

[Riccardo Brasca]

I can just remove master (we have a backup in mathlib3) and rename this one

[Utensil Song]

you may rename this one to main then make main the default branch for github

[Utensil Song]

too divergent to do any merge or rebase

[Riccardo Brasca]

I am doing it.

[Riccardo Brasca]

master is now named master_mathlib3

If you have a local clone, you can update it by running the following commands.

git branch -m master master_mathlib3
git fetch origin
git branch -u origin/master_mathlib3 master_mathlib3
git remote set-head origin -a

[Utensil Song]

The branch name in the workflow also need to be updated.

[Riccardo Brasca]

OK, master is now the mathlib4 version, and it is the default branch

[Riccardo Brasca]

The blue print seems OK

[Utensil Song]

I'll be offline for a while, if anything goes wrong with the blueprint, I can check after an hour or 2.

[Riccardo Brasca]

Also the dependency graph

[Chris Birkbeck]

Utensil Song said:

it's possible that the ghost of old lake causing this

is there a way to fix this?

[Chris Birkbeck]

Riccardo Brasca said:

Also the dependency graph

these will be the old ones.

[Chris Birkbeck]

If you have access to the settings, then under pages select the source to be github actions. That should make it work once the workflow runs

[Riccardo Brasca]

CI is complaining.

[Chris Birkbeck]

hmm the build failed. I think because the lake-manifest doesnt have the doc-gen4

[Chris Birkbeck]

In the blueprint_test the lake-manifest has a few more things that didnt make it over to the merge

[Riccardo Brasca]

Ah OK, feel free to fix it (there was a conflict and I randomly decided what to keep)

[Chris Birkbeck]

Yeah i'll try to fix it, although my build it broken due to the error above which I don't know how to fix

[Riccardo Brasca]

Let me try

[Chris Birkbeck]

It didn't seem to like your first try.

[Riccardo Brasca]

Second try

[Chris Birkbeck]

hmmm ok it failed again and I'm not sure why this time. Let me go back and check the other repo

[Riccardo Brasca]

Can it be the github action thing?

[Riccardo Brasca]

I can modify it.

[Chris Birkbeck]

ok the lakefile.lean also needs to change

[Chris Birkbeck]

it needs to have require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

[Riccardo Brasca]

It is doing something!

[Riccardo Brasca]

Now the error is at "Deploy to GitHub Pages", so I guess it's what you mentioned before. Do you understand what this settings does?

[Chris Birkbeck]

From what I understand it allows the github page to be deployed from the workflow (although that might be wrong)

[Chris Birkbeck]

Did you change that in the settings?

[Riccardo Brasca]

Trying now.

[Utensil Song]

It's slow to build the doc along with full Mathlib. You may add cache of Mathlib docs to save more than half of build time (for doc).

[Utensil Song]

This is how to configure Pages.

[Riccardo Brasca]

The build succeeded, but https://leanprover-community.github.io/flt-regular/ is not working...

[Chris Birkbeck]

try https://leanprover-community.github.io/flt-regular/blueprint/

[Chris Birkbeck]

I updated the links in the readme

[Chris Birkbeck]

but it seems to be working, I still need to fix up the blueprint tex a bit more (like fixing the section titles and adding more details), but at least it seems to be working now :)

[Riccardo Brasca]

Great! I am done for today, but thanks a lot!

[Chris Birkbeck]

No, thank you for deploying it all!

[Riccardo Brasca]

If you have time can you set up the mathlib cache thing? Currently the build takes indeed a lot.

[Chris Birkbeck]

Oh yes let me see if I can figure it out

[Lars Ericson]

A compact, portable representation of the blueprint is available here: https://www.storerch.shop/bnhn

[Utensil Song]

Lars Ericson said:

A compact, portable representation of the blueprint is available here: https://www.storerch.shop/bnhn

Is the LaTeX source of this T-shirt available somewhere?

[Alex J. Best]

If you do want such a t-shirt please buy it from https://promys.org/resources/fermat-t-shirts/ and support the promys foundation, I have no idea who runs that random online shop but it seems unlikely to be such a good cause. @Utensil Song if you email them at that web-address they may be happy to send you the source, they are quite nice people!
Also worth noting this is the blueprint for FLT not FLT-regular.

[Kevin Buzzard]

It's not the blueprint I'm following either :-)

[Ruben Van de Velde]

It's not even blue!