Zulip Chat Archive

Now my file is about 3000 lines, and Lean is way too slow. So I thought the cure is to put the first 2000 lines in
file1.lean and the last 1000 lines in file2.lean and put "import file1" at the top of file2.

But that caused a lot of error messages from file2, such as

All Messages (46)
inf2.lean:3:0
declaration 'lemma9c' uses sorry
inf2.lean:3:29
unknown identifier 'M'

I guess the end of file1 automatically closes a section or a namespace or something. What is the right way
to split my file?

Kyle Miller (Sep 11 2020 at 06:08):

A module is a single file, starting with a list of imports, and then the rest is as if it is contained in an implicit section. The module system is how Lean resolves which code to load for import statements.

A section groups together things like variables, open, and other locally defined things (such as private definitions). Orthogonal to modules, there is a namespace system that groups together definitions under the prefix specified by the namespace declaration -- this also introduces an implicit section for local things. (Namespaces are sort of like Common Lisp packages or Mathematica contexts.) Since a module is as if there is an implicit section, you'll need to open the namespaces you're interested in within each separate module.

I use sections for two reasons: (1) grouping together related definitions for documentation reasons only and (2) to control the current variables and opened namespaces. (By the way, open essentially just copies the definitions within a given namespace into the current section's list of names that can be referenced. There's no corresponding operation of closing a namespace.)

There's a chance some of your errors might be because of stale olean files, so you might need to delete them (and maybe restart Lean? I'm not sure).

Michael Beeson (Sep 11 2020 at 06:17):

If file1 has import xxx at the top and file2 has import file1 at the top then
are things defined in xxx accessible in file2? That is, is "import" transitive?

Patrick Massot (Sep 11 2020 at 06:25):

Yes

Michael Beeson (Sep 11 2020 at 07:20):

OK, I split my file, and it seemed at first to speed up, but then it started going slowly again, i.e., it takes a long time to
process (like 15 seconds or longer) after I type a new proof step, and the fan goes on (meaning all four cores are in use).
What can I do about this?

Kenny Lau (Sep 11 2020 at 07:30):

you can compile the first file into an olean

Kenny Lau (Sep 11 2020 at 07:30):

and whenever everything start compiling again, just restart Lean (Ctrl+Shift+P)

Alex Peattie (Sep 11 2020 at 08:49):

If you're on VSCode too it might be helpful to restrict what files/lines Lean is checking, if you open the Command Palette and type "lean check" you can see the various options (check open files only, check only lines above cursor etc.)

Michael Beeson (Sep 11 2020 at 09:15):

Thanks Alex, command palette helped a lot and only took seconds. I don't know how to compile to olean and will try to learn that tomorrow. Unless command palette makes it unnecessary.