leanpkg ignores

Stream: lean4

[Jason Gross]

How do I tell leanpkg build to ignore files of the form path/to/.#something.lean? Emacs will create this files as temporaries, and I don't want them built

[Sebastian Ullrich]

We could allow specifying more flags at https://github.com/leanprover/lean4/blob/master/src/lean.mk.in#L26, but personally I think a much better solution is to fix the issue for all programs on the Emacs side by setting auto-save-list-file-prefix

[Sebastian Ullrich]

Note that the Nix build system only builds modules reachable from the package root module, but I wouldn't know how to do that with make

[Sebastian Ullrich]

The "basic" build system is in need of some love in general. I don't think we want to stick with make there, but what are the alternatives? Shake? A custom build system built in Lean, much like in Lean 3?

[Jason Gross]

How does setting auto-save-list-file-prefix help?

[Jason Gross]

Note that the Nix build system only builds modules reachable from the package root module

How does nix compute this? Can you replace find $(PKG) -name '*.lean' with some external utility which computes the dependencies?

[Sebastian Ullrich]

Both systems use lean --deps to get the immediate dependencies. Nix then computes the transitive closure in Nix. make could possbly use an external program/script doing just that, yes.

[Sebastian Ullrich]

Jason Gross said:

How does setting auto-save-list-file-prefix help?

It moves Emacs' autosave files out of the way. Thus I don't have to add them to every single .gitignore file, or fight with other issues like this one.

[Jason Gross]

If you want to compute transitive closure in make, you can do something like

read_deps = $(shell lean --deps $1)
transitive_deps = $(if $1,$(call transitive_deps,$(sort $(filter-out $1 $2,$(call read_deps,$1))),$1 $2),$2)

or

transitive_deps = $(if $1,$(call transitive_deps,$(sort $(filter-out $1 $2,$(shell lean --deps $1))),$1 $2),$2)

This assumes there are no spaces in path and file names, btw. Much, much harder to do this if there are spaces.
(This also assumes that lean --deps takes multiple arguments; if not, replace $(shell lean --deps $1) with $(foreach i,$1,$(shell lean --deps $(i))))

The way to read this code is:
define transitive_deps to take two arguments (defaulting to empty if not given). The first argument is the list of files whose deps have not yet been computed; the second is the list of files whose deps have been computed. If the first argument is empty, return the second argument. Otherwise, recursively call transitive_deps as follows: the list of files whose deps are not yet computed should be anything that lean --deps returns on the current first argument which is not already present in either the first or the second arguments (and then sort this list for robustness in argument ordering and return values). The second argument to the recursive call should be everything currently in either the first or the second argument.

[Sebastian Ullrich]

Sounds pretty good. All these paths should be relative to the package root, so spaces should not be an issue unless someone uses very exotic Lean module names. Do you want to give integrating this a try? You don't need to compile Lean from source for this, it should be sufficient to copy lean.mk from the release to a Makefile in the package root and edit it there, where it should be automatically picked up by leanmake/leanpkg.

[Sebastian Ullrich]

Note that we do a bit of post-processing on the output of lean --deps: https://github.com/leanprover/lean4/blob/ea91317f1a29c658ca1b587f4f2ab156efdc07f3/src/lean.mk.in#L50-L52

[Jason Gross]

Hm, when I try to run lean --deps manually on my file, it complains about unknown package. What's required to avoid this failure?

[Sebastian Ullrich]

It depends on LEAN_PATH, set here in lean.mk: https://github.com/leanprover/lean4/blob/ea91317f1a29c658ca1b587f4f2ab156efdc07f3/src/lean.mk.in#L28

[Jason Gross]

Ah, I see. What's $(*D) in https://github.com/leanprover/lean4/blob/ea91317f1a29c658ca1b587f4f2ab156efdc07f3/src/lean.mk.in#L49?

[Sebastian Ullrich]

The directory part of the path matched by %.depend: https://www.gnu.org/software/make/manual/html_node/Automatic-Variables.html#Automatic-Variables

[Sebastian Ullrich]

E.g. A/B for A/B/C.depend

[Jason Gross]

Hm, and these directories need to exist for lean --deps to work

[Jason Gross]

This is an issue, though. How are we to know what directories need to exist without calling lean --deps, which itself fails if the relevant directories don't exist?

[Sebastian Ullrich]

No, only $(OLEAN_OUT)/$(PKG) has to exist for that. The mkdir is so that echo ... > $@ works.

[Sebastian Ullrich]

I hope the overhead of calling lean --deps on every single file of the package on every invocation of leanpkg build is not too big. Nix caches this information on disk, just like the current Makefile does, though I have no idea if that is a significant speedup.

[Sebastian Ullrich]

It looks like it's ~1s on the stdlib, that's not great

[Jason Gross]

We could cache on disk using the following scheme:
If cache does not exist: run lean --deps on all of the files and store the output in cache
Read cache: if cache is older than any of the .lean files in the cache, rebuild cache and read it again

[Sebastian Ullrich]

I fear this feature is getting out of hand. The .depend files are already caching imports, now we're adding a second cache?
Let's maybe take a step back and check where we actually need the set of .lean files:

• It doesn't really matter if we create .depend files for random .lean files as long as this never aborts the build
• For building .olean files, it is sufficient to build $(PKG).olean, which will recursively build all reachable files
• The only other part where we use SRCS is to collect the .o files for compilation of a library/binary. Could we perhaps do this in some other way? Just collecting all .o files in the output directory would not be ideal since it could also collect outputs of since-deleted .lean files.

[Sebastian Ullrich]

I'm assuming here we can't just have make compute the transitive closure with recursive includes starting with include $(PKG).depend. Even if it works I think make would happily visit the same file multiple times.

[Jason Gross]

We could have make compute the transitive closure, but this may be quadratic; after building the relevant included files make will start again from scratch, and it might do this recursively.

[Jason Gross]

• The only other part where we use SRCS is to collect the .o files for compilation of a library/binary. Could we perhaps do this in some other way? Just collecting all .o files in the output directory would not be ideal since it could also collect outputs of since-deleted .lean files.

We could make a "volatile output" directory which we obliterate before compiling the library, and then we recursively copy the .o files?

[Jason Gross]

But, hm, maybe we can avoid at least the issue with visiting files multiple times using the same strategy that C header files use, by wrapping the whole file in an ifndef?

[Jason Gross]

Why are all the slashes doubled on https://github.com/leanprover/lean4/blob/ea91317f1a29c658ca1b587f4f2ab156efdc07f3/src/lean.mk.in#L52 ?

[Jason Gross]

This seems to work:

diff --git a/src/lean.mk.in b/src/lean.mk.in
index 1fb910d965..0755532b93 100644
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -23,33 +23,49 @@ LEAN_OPTS = @LEAN_EXTRA_MAKE_OPTS@
 LEANC_OPTS = -O3 -DNDEBUG
 LINK_OPTS =

-SRCS = $(shell find $(PKG) -name '*.lean' 2> /dev/null || true; find $(PKG).lean 2> /dev/null)
-DEPS = $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.depend))
 export LEAN_PATH += :$(OLEAN_OUT)
-OBJS = $(addprefix $(OLEAN_OUT)/, $(SRCS:.lean=.olean))

 SHELL = /usr/bin/env bash -eo pipefail

 .PHONY: all bin lib depends clean

-all: $(OBJS)
+all: $(OLEAN_OUT)/$(PKG).olean

 bin: $(BIN_OUT)/$(BIN_NAME)

 lib: $(LIB_OUT)/$(STATIC_LIB_NAME)

-depends: $(DEPS)
+# Since we include dependencies in the makefile, we don't need this target to depend on anything
+depends:

 $(OLEAN_OUT)/$(PKG) $(LIB_OUT) $(BIN_OUT):
    @mkdir -p "$@"

 # Make sure the .olean output directory exists so that `lean --deps` knows where this package's
 # .olean files will be located even before any of them are actually built.
+empty=
+space=$(empty) $(empty)
+sanitize_var_name=$(subst .,,$(subst /,,$(subst $(space),,$1)))
 $(TEMP_OUT)/%.depend: %.lean | $(OLEAN_OUT)/$(PKG)
    @mkdir -p "$(TEMP_OUT)/$(*D)"
 # use separate assignment to ensure failure propagation
 # convert path separators and newlines on Windows
-   @deps=`$(LEAN) --deps $< | tr '\\\\' / | tr -d '\\r'`; echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps > $@
+# We want to include only local .depend files, not system ones.
+# For some reason, LEAN_PATH is ././$(OLEAN_OUT), not $(OLEAN_OUT), so
+# we need to remove the leading ./ before filtering for local dependencies.
+# We need || true on the includes because grep will fail if there are
+# no local dependencies.
+   @deps=`$(LEAN) --deps $< | tr '\\\\' / | tr -d '\\r'`; \
+    includes=`echo "$$deps" | tr ' ' '\\n' | grep '^\\(\\./\\)*$(OLEAN_OUT)/' | sed 's,^\\(\\./\\)*$(OLEAN_OUT),$(TEMP_OUT),g; s,\\.olean$$,.depend,g' | tr '\\n' ' ' | sed 's,^,include ,g' || true`; \
+    {                                                                   \
+     echo ifndef $(call sanitize_var_name,$<);                          \
+     echo $(call sanitize_var_name,$<)=;                                \
+     echo $(OLEAN_OUT)/$(<:.lean=.olean): $$deps;                       \
+     echo '$$(BIN_OUT)/$$(BIN_NAME): $(TEMP_OUT)/$(<:.lean=.o)';        \
+     echo '$$(LIB_OUT)/$$(STATIC_LIB_NAME): $(TEMP_OUT)/$(<:.lean=.o)'; \
+     echo $$includes;                                                   \
+     echo endif;                                                        \
+   } > $@

 $(OLEAN_OUT)/%.olean: %.lean $(TEMP_OUT)/%.depend $(MORE_DEPS)
 ifdef CMAKE_LIKE_OUTPUT
@@ -76,7 +92,7 @@ else
    $(LEANC) -c -o $@ $< $(LEANC_OPTS)
 endif

-$(BIN_OUT)/$(BIN_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(BIN_OUT)
+$(BIN_OUT)/$(BIN_NAME): | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
    @echo "[    ] Linking $@"
 endif
@@ -86,7 +102,7 @@ else
    $(LEANC) -o "$@" -x none $^ $(LINK_OPTS)
 endif

-$(LIB_OUT)/$(STATIC_LIB_NAME): $(addprefix $(TEMP_OUT)/,$(SRCS:.lean=.o)) | $(LIB_OUT)
+$(LIB_OUT)/$(STATIC_LIB_NAME): | $(LIB_OUT)
    @rm -f $@
    @ar rcs $@ $^

@@ -95,4 +111,4 @@ clean:

 .PRECIOUS: $(TEMP_OUT)/%.c

-include $(DEPS)
+include $(TEMP_OUT)/$(PKG).depend

[Jason Gross]

I haven't tested how this performs on the standard library, though; going through recursive include might or might not slow down make

[Jason Gross]

Should I make a PR?

[Sebastian Ullrich]

Wow! Not sure if I should be awed or terrified, but since we very rarely have to touch that file, I suppose the maintenance overhead is negligible. But we should definitely test it on the stdlib, yes.

[Sebastian Ullrich]

@Jason Gross Zulip helpfully replaced all tabs with spaces, so I can't apply your patch

[Johan Commelin]

That sounds like a bug in Zulip!

[Sebastian Ullrich]

And the workaround is patch --ignore-whitespace :)

[Sebastian Ullrich]

@Jason Gross I'm afraid this basically doesn't even terminate on the stdlib

[Sebastian Ullrich]

Actually forgot I had it still running

make -C build/release VERBOSE=1  3062.13s user 686.90s system 99% cpu 1:02:29.27 total