Configuration initialization

Stream: lean4

[Yahoo]

QQ图片20250525000510.png
Pls how can this situation be resolved :slight_smile:

[Mario Carneiro]

looks like a network issue. Try restarting it a few times. Can you get to github in your web browser? (China users sometimes have to do other things to make this work)

[Yahoo]

In fact, I deployed all the files I needed locally, but I didn't know where to redirect git commands to pull web pages to local files

[Mario Carneiro]

That particular call is cloning mathlib into .lake/packages/mathlib. I think if you ensure that it is already there and checked out to the same commit as what is in the lockfile then it will skip the step

[Mario Carneiro]

I notice that you also don't have a lockfile in the project hierarchy view, this is lake-manifest.json in the MIL repo. You should get all the files in the repo, don't just get the lean files and drop the metadata

[Mario Carneiro]

the main other file you seem to be missing is lean-toolchain

[Yahoo]

They exist exactly but filtered by the window

[Yahoo]

Mario Carneiro said:

looks like a network issue. Try restarting it a few times. Can you get to github in your web browser? (China users sometimes have to do other things to make this work)

Certainly, but via VPN. Maybe this is one of the reason.

[Yahoo]

@Mario Carneiro I soved it!

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "v4.19.0"

I remove the require code from lakefile.toml, then done

[Mario Carneiro]

uh, that will cause mathlib to not be a dependency which will make the mathlib imports fail

[Mario Carneiro]

what happens when you copy the whole MIL project locally, check out mathlib rev c44e0c8ee63ca166450922a373c7409c5d26b00b to .lake/packages/mathlib, and run lake build at the command line?

[Yahoo]

I just tried to change the git address to the local "mathlib4" directory after a while of operation, but it didn't seem to have any significant effect. I still got an error message like "error: external command 'git' exported with code 128", which left me a bit confused

[Mario Carneiro]

I don't think that will work

[Mario Carneiro]

like I said, you should try to set things up so that it won't call git in the first place

[Mac Malone]

It will always call git (to check the commit hash), but it will not clone anything if it matches the locked revision.

[Mario Carneiro]

I don't know enough about how these VPN setups work, but there should be a way to set up elan, lake and cache to use a VPN if the user has one configured.

[Julian Berman]

git will respect $http_proxy / $https_proxy / $all_proxy environment variables if you have them set, so if you don't, you should set them. There's also git-specific proxy configuration, although if you're on this kind of network connection really you should "Fix" it for all programs so I'd be using the former personally as long as you have a good SOCKS proxy (e.g. some server you can SSH to outside of the firewall). Here's a gist on the latter though (which I have not tested personally): https://gist.github.com/evantoli/f8c23a37eb3558ab8765