From b8557b63af85b5c83af35f76f46549b211d1010b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 May 2020 16:32:35 -0700 Subject: [PATCH] chore: temporary workaround @Kha I had to comment the following lines. It is unclear what is going on. All stages were building on my machine until I tried to build using a fresh `build/release` directory. Then, I managed to reproduce the error in the CI earlier today. So, I destructively removed the `update-stage0`, and tried to build using a fresh `build/release`. Then, I get the following error at stage 1. ``` error: no such file or directory (error code: 2) file: /Users/leonardodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/Std ``` The error seems to be produced by the line I have commented. It is a weird bug since I do have the directory ``` /Users/leonardodemoura/projects/lean4/build/release/stage1/lib/lean/Std ``` Note that it works for ``` /Users/leonardodemoura/projects/lean4/build/release/stage1/bin/../lib/lean/Init` ``` No idea why it doesn't work for `Std`. Anyway, by commenting the lines in this commit I can build all stages locally. The test `binomial.lean` doesn't work since `Std` is not in the builtin path. --- src/Init/Lean/Util/Path.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean index 47da742418..e3e0060e12 100644 --- a/src/Init/Lean/Util/Path.lean +++ b/src/Init/Lean/Util/Path.lean @@ -51,9 +51,10 @@ installedLibDirExists ← IO.isDir installedLibDir; if installedLibDirExists then do initPath ← realPathNormalized installedLibDir; let map := HashMap.empty.insert "Init" initPath; - let stdDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std"; - stdPath ← realPathNormalized stdDir; - pure $ map.insert "Std" stdPath + -- let stdDir := appDir ++ pathSep ++ ".." ++ pathSep ++ "lib" ++ pathSep ++ "lean" ++ pathSep ++ "Std"; + -- stdPath ← realPathNormalized stdDir; + -- let map := map.insert "Std" stdPath; + pure map else pure ∅