Removing FLT_files

Stream: FLT

[Kevin Buzzard]

I promised to Yael that if they changed CI so that it didn't use -Kenv then I'd change the set-up of the project so that it didn't use the FLT_files.lean set-up i.e. I'd move it to FLT.lean. This will also make the project more "standard" in the sense that every Project file seems to have a Project.lean file containing all the files in the project, for better or worse (I still think that this is super-weird because we never had anything like this in the lean 3 days and nobody seemed to be complaining that such a file should exist; all it seems to do as far as I can see is cause inconvenience when people forget to update it when adding a new file).

But I don't really want to lose the current FLT.lean, because I think the name PNat.pow_add_pow_ne_pow is funny and I'd like it to be in the "headline file". So I'm thinking of renaming it to FermatsLastTheorem.lean, importing the weird FLT.lean file at the top of that file, having FLT.lean not import FermatsLastTheorem.lean, and ensuring that lake build builds FermatsLastTheorem.lean. I have two questions.

1) Is such a set-up acceptable to e.g. @Yaël Dillies , who doesn't like the current set-up because it doesn't conform to project standards
2) How do I ensure that lake build builds FermatsLastTheorem.lean?

[Kevin Buzzard]

Possibly related: the docs for lakefile.toml say

TOML
The TOML configuration format is fully declarative. Projects that don't include custom targets, facets, or scripts can use the TOML format. Because TOML parsers are available for a wide variety of languages, using this format facilitates integration with tools that are not written in Lean.

How close am I to being able to use a TOML file for FLT?

[Michael Rothgang]

In many cases, you can must use a toml file. The biggest exception is if your lakefile mentions doc-gen. I don't remember if FLT has that; it's not difficult to change. I've done the same for carleson and sphere-eversion.

[Michael Rothgang]

Actually, I just read the other thread: with Yael's proposed set, I presume you don't have doc-gen in your lakefile anymore. So I would guess (but haven't checked) that the answer is "nothing".

[Ruben Van de Velde]

Yeah, looks like you could adapt https://github.com/fpvandoorn/carleson/blob/master/lakefile.toml pretty easily now

[Yaël Dillies]

Absolutely, we can use a lakefile.toml

[Yaël Dillies]

1. Yes, absolutely. I mostly want to get rid of custom scripts like mk_all.sh so that setting up and maintaining projects becomes easier. Eg I am trying to set up a new project and it's takinf me two days and counting because various bits of automation are mathlib-specific or LeanCamCombi-specific or...

[Yaël Dillies]

2. You can declare it as a build target in the lakefile