command line interface

Stream: new members

[Jiekai]

My vscode lean environment constantly run out of memory. I'm wondering if there is a command line interface?
Here is the my lean file. What command should I use to output the #check result?

import analysis.complex.exponential

open real

#check pi

[Jiekai]

Trying to go through <https://github.com/kbuzzard/xena/blob/master/lean_together/5_minutes_on_type_theory/2_more_type_examples.lean>

[Kevin Buzzard]

Oh my goodness how do people find these random things

[Kevin Buzzard]

Why don't you just fix your VS Code lean environment?

[Kevin Buzzard]

There are commend line options to limit the amount of memory lean uses

[Kevin Buzzard]

And you can tell VS Code to use these options when it invokes Lean

[Marc Huisinga]

if you publish anything on the web, someone's gonna find it ;)

[Kevin Buzzard]

That stuff you stumbled upon is some ideas for scripts for five minute lean videos

[Kevin Buzzard]

I have more not online

[Jiekai]

https://av-media.vu.nl/mediasite/Play/27894c3a8a4d4768a0421f62e5345a6c1d

I'm watching the video :grinning:

[Kevin Buzzard]

Maybe it's time some of those videos got made. The big issue I had with making them is that I want wacky graphics and don't know how to make them

[Kevin Buzzard]

I mean I want something which could easily be knocked up in 5 minutes by someone who knows how to use PowerPoint

[Jiekai]

Looking into the vscode lean server situation, there seems to be some sort of memory leak. The memory lean process uses increases at 100MiB / sec.
The process command:
/home/zjk/.elan/toolchains/leanprover-community-lean-3.5.1/bin/lean --server -M 4096 -T 100000 */home/zjk/github/M4P33*

[Scott Morrison]

Can you provide us a reproducible case to run it on?

[Jiekai]

I think all I did is typing this line then after several seconds commenting it out.

-- import analysis.complex.basic

[Jiekai]

_target/deps/mathlib$ git status
HEAD detached at 8700aa7d
nothing to commit, working tree clean

Not sure if this is relevant.

[Jiekai]

Seems quite reproducible. I change this <https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-node/demo.ts> to

diff --git a/lean-client-js-node/demo.ts b/lean-client-js-node/demo.ts
index 895d0da..1b0071c 100644
--- a/lean-client-js-node/demo.ts
+++ b/lean-client-js-node/demo.ts
@@ -1,6 +1,8 @@
 import * as lean from './src';

-const transport = new lean.ProcessTransport('lean', '.', []);
+const transport = new lean.ProcessTransport(
+  '/home/zjk/.elan/toolchains/leanprover-community-lean-3.5.1/bin/lean',
+  '/home/zjk/github/M4P33', ['-M 4096', '-T 100000']);
 const server = new lean.Server(transport);
 server.error.on((err) => console.log('error:', err));
 server.allMessages.on((allMessages) => console.log('messages', allMessages.msgs));
@@ -8,16 +10,10 @@ server.tasks.on((currentTasks) => console.log('tasks:', currentTasks.tasks));

 server.connect();

-const testfile = ''
-    + 'variables p q r s : Prop\n'
-    + 'theorem my_and_comm : p /\\ q <-> q /\\ p :=\n'
-    + 'iff.intro\n'
-    + '  (assume Hpq : p /\\ q,\n'
-    + '    and.intro (and.elim_right Hpq) (and.elim_left Hpq))\n'
-    + '  (assume Hqp : q /\\ p,\n'
-    + '    and.intro (and.elim_right Hqp) {!!})\n'
-    + '#check @nat.rec_on\n'
-    + '#print "end of file!"\n';
+const testfile = `
+import analysis.complex.basic
+
+`;

 async function demo(): Promise<any> {
     await server.sync('test.lean', testfile);
@@ -34,14 +30,14 @@ async function demo(): Promise<any> {
     }

     const info = await server.info('test.lean', 3, 0);
-    console.log(`got info: ${JSON.stringify(info)}`);
+    // console.log(`got info: ${JSON.stringify(info)}`);
 }

 async function main(): Promise<any> {
     await demo();
-    server.restart();
-    await demo();
-    process.exit(0);
+    // server.restart();
+    // await demo();
+    // process.exit(0);
 }

 main().catch((err) => console.log('error:', err));

Then I have until the process is killed

  PID USER      PR  NI    VIRT    RES    SHR S  %CPU %MEM     TIME+ COMMAND
 1454 zjk       20   0 10.706g 9.749g   9368 S 507.3 62.9  20:52.73 lean
21454 zjk       20   0 11.190g 1.571g  35832 S   1.3 10.1  25:29.84 java

[Scott Morrison]

Can you make sure leanpkg build returns in <30 secs, and post your leanpkg.toml file and the output of ls in your project directory?

[Jiekai]

leanpkg build never returns correctly and uses all memory eventually.

[Jiekai]

My project directory is a cloned https://github.com/ImperialCollegeLondon/M4P33.

[Jiekai]

[package]
name = "M4P33"
version = "0.1"
lean_version = "leanprover-community/lean:3.5.1"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "8700aa7d78b10b65cf8db1d9e320872ae313517a"}

[Jiekai]

$ ls -l
total 44
drwxr-xr-x 2 zjk zjk  4096 3月  26 10:43 doc
-rw-r--r-- 1 zjk zjk    54 3月  28 18:40 leanpkg.path
-rw-r--r-- 1 zjk zjk   237 3月  28 10:33 leanpkg.toml
-rw-r--r-- 1 zjk zjk 11357 3月  26 10:43 LICENSE
drwxr-xr-x 3 zjk zjk  4096 3月  26 10:43 problem_sheets
-rw-r--r-- 1 zjk zjk  1816 3月  26 10:43 README.md
drwxr-xr-x 6 zjk zjk  4096 3月  28 18:40 src
drwxr-xr-x 3 zjk zjk  4096 3月  27 17:04 _target
-rw-r--r-- 1 zjk zjk   266 3月  26 10:43 TODO.txt

[Jiekai]

Oh. leanpkg build finished. Seems that in the previous run I just give up when memory usage hit 4Gib and killed leanpkg build.

[Jiekai]

Now it all seems working. Thank you! So leanpkg build is crucial.

[Kevin Buzzard]

Nobody should be using leanpkg any more

[Kevin Buzzard]

If you install the project with leanproject do you get the same problems? This should download a compiled mathlib

[Jiekai]

Anywhere I can learn about difference betweenleanpkg and leanproject?

[Kevin Buzzard]

Leanproject handles projects which aren't on 3.4.2 like the M4P33 one

[Patrick Massot]

@Kevin Buzzard this project is not so old, it actually has available mathlib olean (although they are still on GitHub, so API limiting rate may strike). Could you change the README to tell people to leanproject get ImperialCollegeLondon/M4P33?

[Kevin Buzzard]

Oh sure! I hadn't realised it was my fault

[Kevin Buzzard]

I should do this for all my repos

[Patrick Massot]

By the way, I'm working on the weird message about not being in a Git repository. I totally understand where it comes from. The problem is that fetching oleans from GitHub instead of Azure is half deprecated, still supported by mathlibtools but not well tested.