Use `leanc` written in Lean for testing & distribution #687

Kha · 2021-09-24T14:21:25Z

Building is still handled by a (minimal) Bash script for bootstrapping purposes

building is still handled by a (minimal) Bash script for bootstrapping purposes

lovettchris · 2021-09-24T17:18:38Z

src/CMakeLists.txt

@@ -325,7 +325,7 @@ endif()
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
  # import library created by the `leanshared` target
-  set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} $bindir/libleanshared.dll.a")
+  set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -lleanshared")


why cant this library dependency be a cmake target DEPENDS ? is it because "leanshared" is not a cmake "add_library" somewhere? If so, why isn't it?

This flag is baked into leanc, i.e. user programs are linked with it as well

I see thanks.

By the way the title of this PR confuses me, "testing & distribution", isn't stdlib.make a central part of the regular build too? What does "distribution" mean?

Distribution means what we ship to users, i.e. the release tarballs created by cpack

lovettchris · 2021-09-24T17:42:44Z

src/Leanc.lean

+  if args.isEmpty then
+    IO.println "Lean C compiler
+
+A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`,


This is cool, are you moving bash shell scripts to lean? That's awesome, and will make one day building on windows easier right? Do we still need nix if we use Lean like this? Is this what Lake is ?

We never needed Nix :) . It's always been an alternative setup. But this + #659 + #683 will mean that we have a self-contained build system (for Lean packages, not Lean itself) without any GNU dependencies, yes.

lovettchris · 2021-09-24T17:44:09Z

src/bin/leanc.in

-$LEAN_CC "${cflags[@]}" "${args[@]}" "${ldflags_ext[@]}" "${ldflags[@]}" -Wno-unused-command-line-argument
+# used only for building Lean itself
+root=$(dirname $0)
+${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ -Wno-unused-command-line-argument


do we really still need this leanc.sh then? Can't we just move this line into the place that calls it? I think that's only stdlib.make.in right?

We could, yes. It wouldn't exactly be pretty, and it makes it easier to communicate the flags to Nix.

tydeu · 2021-09-25T18:07:35Z

@Kha looking at the simplicity of leanc makes me wonder whether it should instead just be part of Lake? That is, I could just add a lake cc/lake ld commands that does the same thing as leanc and no longer need to call out to an external leanc process when building Lean modules.

In order to keep things in sync, the built-in settings for leanc (i.e., LEAN_CC, LEANC_EXTRA_FLAGS, etc.) could be in a Lean.C (or Leanc) module shipped with Lean. That way they could easily change as Lean changes without often having to simultaneously update Lake.

Also, it seems to me like --print-cflags and --print-ldflags could be merged into the lean itself.

Kha · 2021-09-25T21:41:13Z

I considered it, but I didn't really see the point. Unless process creation on Windows is that slow.

tydeu · 2021-09-25T21:56:31Z

@Kha In my view, such a solutions provides the following benefits:

It allows the leanc wrapper options (e.g., -shared) to be properly typed terms rather than strings (e.g., in Lake)
The default options would be know at a Lean level, rather than being built into the executable
Allows easier separation of the C compiler and linker in Lake (allowing end users to potentially configure both separately)
- Useful if people write different backends (i.e., emitting LLVM bytecode/assembly rather than C)
Removes the need for a separate leanc executable (once Lake is packaged with Lean)

Kha · 2021-10-02T14:01:36Z

We can reevaluate the design when lake is the default

tydeu · 2021-10-02T14:55:47Z

@Kha Fair enough. However, I did come up with one more reason in the meantime. I'll put it here so I don't forget it.

One of the changes on my list is to make the compiler a target as well. This will make its hash part of the trace of targets which use it. Thus, they will be automatically rebuilt when the compiler binary changes. However, the hash of the current leanc would not change when the wrapped compiler changes versions. Even then, lake could still be smart and special case on leanc and use the hash of wrapped compiler as well. However, I think at that point, the overhead would likely be greater than just merging leanc into lake.

Just something to keep in mind for the future.

Kha · 2021-10-02T15:08:12Z

Ok, makes sense

This makes the `a b c` in `cases' foo with a b c` get hovers and syntax highlighting for the variables that were introduced.

chore: put import library in lib/lean/

0ec42cb

Kha force-pushed the lean-leanc branch 2 times, most recently from 6855d0a to 3475698 Compare September 24, 2021 15:05

feat: use leanc written in Lean for testing & distribution

4bb75b3

building is still handled by a (minimal) Bash script for bootstrapping purposes

Kha force-pushed the lean-leanc branch from 3475698 to 4bb75b3 Compare September 24, 2021 16:35

lovettchris reviewed Sep 24, 2021

View reviewed changes

Kha merged commit e692725 into leanprover:master Sep 25, 2021

Kha deleted the lean-leanc branch September 25, 2021 21:42

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022

feat: local variable info on cases' args (leanprover#687)

8fbfbef

This makes the `a b c` in `cases' foo with a b c` get hovers and syntax highlighting for the variables that were introduced.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use `leanc` written in Lean for testing & distribution #687

Use `leanc` written in Lean for testing & distribution #687

Kha commented Sep 24, 2021

lovettchris Sep 24, 2021

Kha Sep 24, 2021

lovettchris Sep 24, 2021

lovettchris Sep 24, 2021

Kha Sep 25, 2021

lovettchris Sep 24, 2021

Kha Sep 25, 2021

lovettchris Sep 24, 2021

Kha Sep 25, 2021

tydeu commented Sep 25, 2021 •

edited

Loading

Kha commented Sep 25, 2021

tydeu commented Sep 25, 2021 •

edited

Loading

Kha commented Oct 2, 2021

tydeu commented Oct 2, 2021

Kha commented Oct 2, 2021

Use leanc written in Lean for testing & distribution #687

Use leanc written in Lean for testing & distribution #687

Conversation

Kha commented Sep 24, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tydeu commented Sep 25, 2021 • edited Loading

Kha commented Sep 25, 2021

tydeu commented Sep 25, 2021 • edited Loading

Kha commented Oct 2, 2021

tydeu commented Oct 2, 2021

Kha commented Oct 2, 2021

Use `leanc` written in Lean for testing & distribution #687

Use `leanc` written in Lean for testing & distribution #687

tydeu commented Sep 25, 2021 •

edited

Loading

tydeu commented Sep 25, 2021 •

edited

Loading