Zulip Chat Archive

Stream: lean4

Topic: leanpkg ignores


view this post on Zulip Jason Gross (Mar 11 2021 at 19:41):

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

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 15:40):

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

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 15:42):

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

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 15:43):

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?

view this post on Zulip Jason Gross (Mar 15 2021 at 17:43):

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

view this post on Zulip Jason Gross (Mar 15 2021 at 17:48):

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?

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 17:51):

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.

view this post on Zulip Sebastian Ullrich (Mar 15 2021 at 17:52):

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.

view this post on Zulip Jason Gross (Mar 15 2021 at 17:59):

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.

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 11:07):

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.

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 11:13):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 13:17):

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

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:22):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 13:23):

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

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:25):

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

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:25):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 13:27):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 13:30):

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?

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:39):

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

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:44):

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.

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 13:48):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 14:06):

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

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 14:27):

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.

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 14:32):

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.

view this post on Zulip Jason Gross (Mar 16 2021 at 14:58):

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.

view this post on Zulip Jason Gross (Mar 16 2021 at 15:09):

  • 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?

view this post on Zulip Jason Gross (Mar 16 2021 at 15:09):

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?

view this post on Zulip Jason Gross (Mar 16 2021 at 15:15):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 15:43):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 15:52):

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

view this post on Zulip Jason Gross (Mar 16 2021 at 15:52):

Should I make a PR?

view this post on Zulip Sebastian Ullrich (Mar 16 2021 at 15:54):

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.

view this post on Zulip Sebastian Ullrich (Mar 17 2021 at 09:23):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 09:24):

That sounds like a bug in Zulip!

view this post on Zulip Sebastian Ullrich (Mar 17 2021 at 09:24):

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

view this post on Zulip Sebastian Ullrich (Mar 17 2021 at 10:42):

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

view this post on Zulip Sebastian Ullrich (Mar 17 2021 at 11:44):

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

Last updated: May 18 2021 at 23:14 UTC