mathematics-in-lean

Stream: new members

[Victor Miller]

I'm trying to get the mathematics-in-lean to use on my mac. I have everything installed, and have successfully gotten other lean projects. However, when I do

leanproject get mathematics-in-lean

the following happens

leanproject get mathematics-in-lean
Cloning from git@github.com:leanprover-community/mathematics-in-lean.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/mathematics-in-lean.git
Username for 'https://github.com':

Why is it asking for a user name, and which one do I use?

[Bryan Gin-ge Chen]

You need to run leanproject get mathematics_in_lean (with underscores).

[Victor Miller]

Thanks. The error message leaves a bit to be desired :-).

[Bryan Gin-ge Chen]

(I'm guessing the reason it's asking for a user name is that something thinks that the 404 message could indicate that the repository is private and only visible after login.)

[Felix Sauter]

Hi guys,
I'm having touble with running may first lean code.
It's a S02_Overview.lean from mathematics_in_lean and i have no idea how i can fix this problem:

c:\Users\felix\.elan\toolchains\leanprover--lean4---v4.8.0-rc2\bin\lake.exe setup-file C:/Users/felix/OneDrive/Desktop/Lernen/4. Semseter/Lean/mathematics_in_lean/MIL/C01_Introduction/S02_Overview.lean Init MIL.Common --no-build failed:

stderr:
✖ [418/2003] Replaying ProofWidgets.Component.Basic
trace: .> LEAN_PATH=.\.\.lake/packages\batteries\.lake\build\lib;.\.\.lake/packages\Qq\.lake\build\lib;.\.\.lake/packages\aesop\.lake\build\lib;.\.\.lake/packages\proofwidgets\.lake\build\lib;.\.\.lake/packages\Cli\.lake\build\lib;.\.\.lake/packages\importGraph\.lake\build\lib;.\.\.lake/packages\mathlib\.lake\build\lib;.\.\.lake\build\lib PATH c:\Users\felix\.elan\toolchains\leanprover--lean4---v4.8.0-rc2\bin\lean.exe .\.\.lake/packages\proofwidgets\.\.\ProofWidgets\Component\Basic.lean -R .\.\.lake/packages\proofwidgets\.\. -o .\.\.lake/packages\proofwidgets\.lake\build\lib\ProofWidgets\Component\Basic.olean -i .\.\.lake/packages\proofwidgets\.lake\build\lib\ProofWidgets\Component\Basic.ilean -c .\.\.lake/packages\proofwidgets\.lake\build\ir\ProofWidgets\Component\Basic.c --json
info: stderr:
failed to create file '.\.\.lake/packages\proofwidgets\.lake\build\lib\ProofWidgets\Component\Basic.olean'
error: Lean exited with code 1
Some builds logged failures:

• ProofWidgets.Component.Basic
  error: build failed

[Mauricio Collares]

As a first step, try closing VS Code, deleting the .lake folder (inside the mathematics_in_lean folder) and re-running lake exe cache get, and re-opening VS Code.

[Mauricio Collares]

(which is another way of saying "I don't know why it failed to create the file, but maybe it was a transient failure")

[Felix Sauter]

Thanks, building everyithing again worked after giving the running process in VSCode full permission for the mathematics_in_lean folder