max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: temporary workaround

Browse source 
@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.
This commit is contained in:
Leonardo de Moura 2020-05-22 16:32:35 -07:00
parent a2e339e868
commit b8557b63af
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Lean/Util/Path.lean
View file

@ -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 ∅