Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Lake build with dependencies require internet access #104

Closed
lecopivo opened this issue Jul 15, 2022 · 2 comments
Closed

Lake build with dependencies require internet access #104

lecopivo opened this issue Jul 15, 2022 · 2 comments
Labels
bug Something isn't working
Milestone

Comments

@lecopivo
Copy link

lecopivo commented Jul 15, 2022

Having mathlib4 as a dependency seems to break lake build if you are offline.


Reproduce:

In a clean directory:

lake init Test

Add the following to lakefile.lean

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"8f609e0ed826dde127c8bc322cb6f91c5369d37a"

Run lake build for initial build and initialization of mathlib4.

Disconnect from the internet and run lake build again, results in:

error: stderr:
fatal: unable to access 'https://github.com/leanprover-community/mathlib4.git/': Could not resolve host: github.com
error: git exited with code 128

Tested on: leanprover/lean4:nightly-2022-07-11

@tydeu tydeu added the bug Something isn't working label Jul 15, 2022
@tydeu tydeu closed this as completed in 398a9e7 Jul 15, 2022
@lecopivo
Copy link
Author

Thanks for fixing this!

@tydeu tydeu added this to the v3.2.2 milestone Jul 15, 2022
@tydeu tydeu modified the milestones: v3.2.2, v3.3.0 Jul 24, 2022
@pechersky
Copy link

I've hit this issue again, with mathlib4 and nightly 2022-10-20, when offline. This prevents the lakefile from parsing, which prevents me from being able to work on porting even when I'm offline.

Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
also add some warnings on url/manifest mismatch + other minor cleanup

closes leanprover/lake#104
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants