Merge branch 'master' into go-to-instance

.github/workflows/ci.yml

@@ -157,10 +157,17 @@ jobs:
           # open nix-shell once for initial setup
           true
         if: matrix.os == 'ubuntu-latest'
+      - name: Set up core dumps
+        run: |
+          mkdir -p $PWD/coredumps
+          # store in current directory, for easy uploading together with binary
+          echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
+        if: matrix.os == 'ubuntu-latest'
       - name: Build
         run: |
           mkdir build
           cd build
+          ulimit -c unlimited # coredumps
           OPTIONS=()
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
@@ -203,6 +210,7 @@ jobs:
       - name: Test
         run: |
           cd build/stage1
+          ulimit -c unlimited # coredumps
           # exclude nonreproducible test
           ctest -j4 --output-on-failure -E leanlaketest_git ${{ matrix.CTEST_OPTIONS }} < /dev/null
         if: ${{ !matrix.cross }}
@@ -212,11 +220,13 @@ jobs:
       - name: Build Stage 2
         run: |
           cd build
+          ulimit -c unlimited # coredumps
           make -j4 stage2
         if: matrix.build-stage2 || matrix.check-stage3
       - name: Check Stage 3
         run: |
           cd build
+          ulimit -c unlimited # coredumps
           make -j4 check-stage3
         if: matrix.check-stage3
       - name: Test Speedcenter Benchmarks
@@ -229,10 +239,31 @@ jobs:
       - name: Check rebootstrap
         run: |
           cd build
+          ulimit -c unlimited # coredumps
           make update-stage0 && make -j4
         if: matrix.name == 'Linux'
       - name: CCache stats
         run: ccache -s
+      - name: Show stacktrace for coredumps
+        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        run: |
+          for c in coredumps/*; do
+            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
+            echo bt | $GDB/bin/gdb -q $progbin $c || true
+          done
+      - name: Upload coredumps
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        with:
+          name: coredumps-${{ matrix.name }}
+          path: |
+            ./coredumps
+            ./build/stage0/bin/lean
+            ./build/stage0/lib/lean/libleanshared.so
+            ./build/stage1/bin/lean
+            ./build/stage1/lib/lean/libleanshared.so
+            ./build/stage2/bin/lean
+            ./build/stage2/lib/lean/libleanshared.so
 
   release:
     if: startsWith(github.ref, 'refs/tags/')

.github/workflows/nix-ci.yml

@@ -81,14 +81,13 @@ jobs:
           skipPush: true  # we push specific outputs only
       - name: Build
         run: |
-          # .o files are not a runtime dependency on macOS because of lack of thin archives
-          nix build $NIX_BUILD_ARGS .#stage0 .#stage1.lean-all .#Lean.oTree .#iTree .#modDepsFiles -o push-build
+          nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
           nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
         if: matrix.name == 'Nix Linux'
       - name: Push to Cachix

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* [Pretty-print signatures in hover and `#check <ident>`](https://github.com/leanprover/lean4/pull/1943).
+
 * [Update Lake to latest prerelease](https://github.com/leanprover/lean4/pull/1879).
 
 * [Introduce parser memoization to avoid exponentional behavior](https://github.com/leanprover/lean4/pull/1799).

doc/examples/widgets.lean

@@ -126,9 +126,10 @@ as seen in the goal view. We will use it to implement our custom `#check` displa
 ⚠️ WARNING: Like the other widget APIs, the infoview JS API is **unstable** and subject to breaking changes.
 
 The code below demonstrates useful parts of the API. To make RPC method calls, we use the `RpcContext`.
-The `useAsync` helper packs the results of a call into a `status` enum, the returned `val`ue in case
-the call was successful, and otherwise an `err`or. Based on the `status` we either display
-an `InteractiveCode`, or `mapRpcError` the error in order to turn it into a readable message.
+The `useAsync` helper packs the results of a call into an `AsyncState` structure which indicates
+whether the call has resolved successfully, has returned an error, or is still in-flight. Based
+on this we either display an `InteractiveCode` with the type, `mapRpcError` the error in order
+to turn it into a readable message, or show a `Loading..` message, respectively.
 -/
 
 @[widget]
@@ -137,21 +138,21 @@ def checkWidget : UserWidgetDefinition where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
-import { RpcContext, InteractiveCode } from '@leanprover/infoview';
+import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
 
 export default function(props) {
   const rs = React.useContext(RpcContext)
   const [name, setName] = React.useState('getType')
-  const [value, setValue] = React.useState(undefined)
 
-  function run() {
-    rs.call('getType', { name, pos: props.pos }).then(setValue)
-  }
+  const st = useAsync(() =>
+    rs.call('getType', { name, pos: props.pos }), [name, rs, props.pos])
 
-  React.useEffect(() => run(), [name])
-  const type = value &&  e(InteractiveCode, {fmt: value})
+  const type = st.state === 'resolved' ? st.value && e(InteractiveCode, {fmt: st.value})
+    : st.state === 'rejected' ? e('p', null, mapRpcError(st.error).message)
+    : e('p', null, 'Loading..')
   const onChange = (event) => { setName(event.target.value) }
-  return e('div', null, e('input', { value: name, onChange }), ' : ', type)
+  return e('div', null,
+    e('input', { value: name, onChange }), ' : ', type)
 }
 "
 
@@ -189,11 +190,9 @@ To do this, use the `React.useContext(EditorContext)` React context.
 This will return an `EditorConnection` whose `api` field contains a number of methods to
 interact with the text editor.
 
-You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/1edd92230c7630627f18dbe76cd139903a4cbcee/lean4-infoview-api/src/infoviewApi.ts#L52)
-
+You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
 -/
 
-
 @[widget]
 def insertTextWidget : UserWidgetDefinition where
   name := "textInserter"

doc/flake.nix

@@ -78,22 +78,30 @@
           (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
         doCheck = false;
       };
-      renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
-        mkdir -p $(basename $out/${name})
-        alectryon --frontend lean4+markup ${file} --backend webpage -o $out/${name}.md
-      '';
-      listFilesRecursiveRel = root: dir: lib.flatten (lib.mapAttrsToList (name: type:
-        if type == "directory" then
-          listFilesRecursiveRel root ("${dir}/${name}")
-        else
-          dir + "/${name}"
-      ) (builtins.readDir "${root}/${dir}"));
-      renderDir = dir: let
-        inputs = builtins.filter (n: builtins.match ".*\.lean" n != null) (listFilesRecursiveRel dir ".");
-        outputs = lib.genAttrs inputs (n: renderLean n "${dir}/${n}");
-      in
-        outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
-      inked = renderDir ./.;
+      renderLeanMod = mod: mod.overrideAttrs (final: prev: {
+        name = "${prev.name}.md";
+        buildInputs = prev.buildInputs ++ [ alectryon ];
+        outputs = [ "out" ];
+        buildCommand = ''
+          dir=$(dirname $relpath)
+          mkdir -p $dir out/$dir
+          if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
+          alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
+        '';
+      });
+      renderPackage = pkg: symlinkJoin {
+        name = "${pkg.name}-mds";
+        paths = map renderLeanMod (lib.attrValues pkg.mods);
+      };
+      literate = buildLeanPackage {
+        name = "literate";
+        src = ./.;
+        roots = [
+          { mod = "examples"; glob = "submodules"; }
+          { mod = "monads"; glob = "submodules"; }
+        ];
+      };
+      inked = renderPackage literate;
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;

doc/monads/intro.md

@@ -32,7 +32,7 @@ Now that you have an intuition for how abstract structures work, you'll examine
 that functors and applicative functors don't help you solve. Then you'll learn the specifics of how
 to actually use monads with some examples using the `Option` monad and the all important `IO` monad.
 
-## [Reader Monads](readers.lean.md)
+## [Reader Monad](readers.lean.md)
 Now that you understand the details of what makes a monadic structure work, in this section, you'll
 learn about one of the most useful built in monads `ReaderM`, which gives your programs a
 global read-only context.

nix/bootstrap.nix

@@ -1,9 +1,10 @@
 { debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages,
+  stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
   ... } @ args:
 with builtins;
 rec {
   inherit stdenv;
+  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
   buildCMake = args: stdenv.mkDerivation ({
     nativeBuildInputs = [ cmake ];
     buildInputs = [ gmp llvmPackages.llvm ];
@@ -15,8 +16,8 @@ rec {
       patchShebangs .
     '';
   } // args // {
-    src = args.realSrc or (lib.sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
-    cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DLLVM=ON" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
+    src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
+    cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
     preConfigure = args.preConfigure or "" + ''
       # ignore absence of submodule
       sed -i 's!lake/Lake.lean!!' CMakeLists.txt
@@ -25,7 +26,7 @@ rec {
   lean-bin-tools-unwrapped = buildCMake {
     name = "lean-bin-tools";
     outputs = [ "out" "leanc_src" ];
-    realSrc = lib.sourceByRegex ../src [ "CMakeLists\.txt" "cmake.*" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ];
+    realSrc = sourceByRegex ../src [ "CMakeLists\.txt" "cmake.*" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ];
     preConfigure = ''
       touch empty.cpp
       sed -i 's/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt
@@ -44,19 +45,15 @@ rec {
   leancpp = buildCMake {
     name = "leancpp";
     src = ../src;
-    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" "runtime_bc" ];
+    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ];
     installPhase = ''
       mkdir -p $out
       mv lib/ $out/
       mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib
-      mv runtime/libleanrt_initial-exec.a runtime/lean.h.bc $out/lib
+      mv runtime/libleanrt_initial-exec.a $out/lib
     '';
   };
-  # rename derivation so `nix run` uses the right executable name but we still see the stage in the build log
-  wrapStage = stage: runCommand "lean" {} ''
-    ln -s ${stage} $out
-  '';
-  stage0 = wrapStage (args.stage0 or (buildCMake {
+  stage0 = args.stage0 or (buildCMake {
     name = "lean-stage0";
     realSrc = ../stage0/src;
     debug = stage0debug;
@@ -75,7 +72,8 @@ rec {
       done
       otool -L $out/bin/lean
     '';
-  }));
+    meta.mainProgram = "lean";
+  });
   stage = { stage, prevStage, self }:
     let
       desc = "stage${toString stage}";
@@ -105,6 +103,7 @@ rec {
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
       stdlib = [ Init Lean ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
+      depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
@@ -119,14 +118,14 @@ rec {
       '';
       mods = Init.mods // Lean.mods;
       leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable.override { withSharedStdlib = true; }}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
       '';
       lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
         mkdir -p $out/bin
         ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
       '';
       # derivation following the directory layout of the "basic" setup, mostly useful for running tests
-      lean-all = wrapStage(stdenv.mkDerivation {
+      lean-all = stdenv.mkDerivation {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
@@ -136,7 +135,13 @@ rec {
           # NOTE: `lndir` will not override existing `bin/leanc`
           ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
         '';
-      });
+        meta.mainProgram = "lean";
+      };
+      cacheRoots = linkFarmFromDrvs "cacheRoots" [
+        stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
+        # .o files are not a runtime dependency on macOS because of lack of thin archives
+        Lean.oTree
+      ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex ../. [ "src.*" "tests.*" ];