Finding (deterministic) timeout

Stream: general

[Floris van Doorn]

I made a change that created a (deterministic) timeout while working on PR #1319. Lean is not very good reporting this error message:

• Travis failed with the error /home/travis/scripts/travis_long: fork: Cannot allocate memory. This was almost certainly because it ran across the timeout
• When running lean --make src/ the deterministic timeout failed silently. The first error message I received was in a file importing the file with the deterministic timeout (it did not create a .olean file for the file with the timeout).
• Suppose A.lean has a deterministic timeout and you open B.lean in VSCode. B.lean does not raise any errors, not even imported file uses sorry.

This made it tricky to find the file with the deterministic timeout. This post is mostly a cautionary tale. But if anyone knows a good way to find which file has the timeout, I'm happy to hear it. (on Windows lean doesn't report which file it is currently compiling, that might help)

[Simon Hudon]

Using a Makefile to build mathlib might help

[Simon Hudon]

I have a Makefile for it somewhere on my drive

[Floris van Doorn]

What is the difference of building mathlib with a Makefile and doing it without?

[Kevin Buzzard]

I thought you approved of automation? :-)

[Patrick Massot]

Are we talking about the benefit of have to type only make instead of leanpkg build?

[Simon Hudon]

In this context, I'm suggesting that using make will let you see what file Lean is currently building. You should get a better idea of where the error is coming from

[Simon Hudon]

I thought you approved of automation? :-)

@Kevin Buzzard I'm not following

[Kevin Buzzard]

We can automate the use of leanpkg so we don't have to remember all those pesky extra inputs like build

[Kevin Buzzard]

Oh! You think make will solve the issue of Windows not printing out file names?

[Kevin Buzzard]

I was just being daft.

[Simon Hudon]

Haha! That's a more liberal use of the word "automation" than I'm used to

[Kevin Buzzard]

I'm a mathematician, what do I know about automation.

[Floris van Doorn]

In this context, I'm suggesting that using make will let you see what file Lean is currently building. You should get a better idea of where the error is coming from

I am very interested in this. How do I get/generate said Makefile?

[Simon Hudon]

Here is the version I found:

SRCS = $(wildcard */*.lean */*/*.lean */*/*/*.lean */*/*/*/*.lean)
OBJS = $(SRCS:.lean=.olean)
DEPS = $(SRCS:.lean=.depend)

.PHONY: all clean

all: $(OBJS)

depends: $(DEPS)

%.depend: %.lean
    @echo $(<:.lean=.olean): `~/lean/lean-master/bin/lean --deps $< | python relative.py`  > $@

# %.depend: ;

%.olean: %.lean %.depend
    sccache lean --make $<
#   sccache lean --make $<

clean:
    find . -name *.olean -delete
    find . -name *.depend -delete

.PRECIOUS: %.depend

include $(DEPS)

It could be better but it works well enough for me

[Simon Hudon]

Basically, it has a pass to generate dependencies and then uses those to build in the proper order

[Floris van Doorn]

So I made a file Makefile with those contents in the mathlib/ directory, but make isn't working. Any idea why?

Floris@MSI MINGW64 /d/projects/mathlib (use_localized)
$ make
Makefile:17: *** missing separator.  Stop.

Floris@MSI MINGW64 /d/projects/mathlib (use_localized)
$ make --version
GNU Make 4.2.1
Built for Windows32
Copyright (C) 1988-2016 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

[Kevin Buzzard]

Shouldn't it say leanpkg build somewhere?

[Patrick Massot]

Kevin... don't be so trivial

[Kevin Buzzard]

FWIW I get the same error on Ubuntu

[Simon Hudon]

Ok, I should have looked at the file a bit more closely. I need to make a couple of fixes

[Simon Hudon]

Here is the new version and a python script that needs to be next to the Makefile

Makefile
relative.py

[Floris van Doorn]

I'm getting a bunch of errors of the form

Traceback (most recent call last):
  File "relative.py", line 9, in <module>
    print(os.path.relpath(x))
  File "C:\Users\Floris\AppData\Local\Programs\Python\Python37-32\lib\ntpath.py", line 562, in relpath
    path_drive, start_drive))
ValueError: path is on mount 'C:', start on mount 'D:'

is that easy to fix?
Thanks for all your efforts btw!

[Wojciech Nawrocki]

Here is Lean 4's relative.py with maybe more cross-platform support

[Simon Hudon]

I think it's the same file. They took it from me.

[Simon Hudon]

@Floris van Doorn Do you have symbolic links mapping paths in D: to drive C:?

[Simon Hudon]

In relative.py, can you add a print statement just before the call to relpath? I'd like to see if something odd is going on in that path. Also, can you print the current directory?

[Floris van Doorn]

@Simon Hudon I think the problem is that my mathlib is in D:\projects\mathlib and my standard library is here: C:\Users\Floris\.elan\toolchains\3.4.2\lib\lean\library\

An example generated file is:

src/tactic/omega/nat/dnf.olean: src\tactic\omega\clause.olean

 src\tactic\omega\nat\form.olean

note: it is missing the import of lean\library\init\default.olean.

If I print x first in your script, I get outputs like

D:\projects\mathlib\src\tactic\omega\nat\form.olean
C:\Users\Floris\.elan\toolchains\3.4.2\lib\lean\library\init\default.olean

[Simon Hudon]

Maybe what we should do is add an if statement before the print to check if x is located in the current directory. We would just print it as is if not.

[Floris van Doorn]

I do not have any (relevant) symbolic links IIRC.
print(os.path.realpath(os.curdir)) gives D:\projects\mathlib.

[Floris van Doorn]

@Wojciech Nawrocki that version indeed has some cross-platform support, and seems to generate all the .depend files. Thanks!
However, in the .depends file it is not correctly replacing backslashes by slahes. Here is an example file generated by the the Lean 4 relative.py:

archive/cubing_a_cube.olean: ..\..\d\projects\mathlib\src\data\real\basic.olean
 ..\..\d\projects\mathlib\src\data\set\disjointed.olean
 ..\..\d\projects\mathlib\src\data\set\intervals.olean
 ..\..\d\projects\mathlib\src\set_theory\cardinal.olean
 ..\..\c\Users\Floris\.elan\toolchains\3.4.2\lib\lean\library\init\default.olean

[Floris van Doorn]

What are the .depend files supposed to look like?
I managed to hack the Python script so forward slashes are used:

archive/cubing_a_cube.olean: ../../d/projects/mathlib/src/data/real/basic.olean
 ../../d/projects/mathlib/src/data/set/disjointed.olean
 ../../d/projects/mathlib/src/data/set/intervals.olean
 ../../d/projects/mathlib/src/set_theory/cardinal.olean
 ../../c/Users/Floris/.elan/toolchains/3.4.2/lib/lean/library/init/default.olean

but I still get the (weird) error message:

Floris@MSI MINGW64 /d/projects/mathlib (use_localized)
$ make
', needed by 'archive/cubing_a_cube.olean'.  Stop./mathlib/src/data/real/basic.olean

[Simon Hudon]

what if you put the paths in quotes? Also, those paths should be on the same line.

[Floris van Doorn]

Quotes didn't help, but it did complain when the paths were not on the same line. After a lot of trial and error the following relative.py works for me. I also got errors when any core library paths were printed, so I don't print them.

import sys
import os
import re

mathlib = os.path.realpath(os.curdir)
mathlib = re.sub(r"^(\w):", lambda m: "/" + m[1].lower(), mathlib).replace('\\', '/').strip()
if mathlib[-1] != '/':
  mathlib += "/"
s = ""

for x in sys.stdin:
  x = re.sub(r"^(\w):", lambda m: "/" + m[1].lower(), x).replace('\\', '/').strip()
  if x.startswith(mathlib):
    s += x[len(mathlib):]
    s += " "

print(s)

[Floris van Doorn]

The error excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold) is also not reported on the command line :sad: (is that a Windows-specific thing?)
The makefile helps a bit though: I can open all files that are slow to compile in VSCode.

[Simon Hudon]

I also got errors when any core library paths were printed, so I don't print them.

That doesn't bode well for when you link various projects together.

[Simon Hudon]

I can open all files that are slow to compile in VSCode.

You could call lean using timeout. Then make decides which ones take long.