Does importing dependency as git repository clone submodules

Stream: new members

[Srayan Jana]

Title says it all.
If i have a Lean project that I want to import as a git repo, will it also import all of the submodules as well?

[Aaron Liu]

no I don't think so

[Aaron Liu]

I guess it depends on what you mean by "import as a git repo"

[Srayan Jana]

@Aaron Liu Like as part of the lakefile
https://lean-lang.org/doc/reference/4.19.0/Build-Tools-and-Distribution/Lake/#The-Lean-Language-Reference--Build-Tools-and-Distribution--Lake--Configuration-File-Format--Lean-Format--Dependencies

[Aaron Liu]

I don't think that imports anything by itself

[Srayan Jana]

https://lean-lang.org/doc/reference/4.19.0/Build-Tools-and-Distribution/Lake/#The-Lean-Language-Reference--Build-Tools-and-Distribution--Lake--Configuration-File-Format--Declarative-TOML-Format--Dependencies

[Aaron Liu]

it just adds the dependency to your project

[Srayan Jana]

Yeah does that dependency include git submodules?

[Srayan Jana]

[[require]] name = "example" git = "https://git.example.com/example.git" rev = "main" version = "2.12"

[Aaron Liu]

so when building your project lake will checkout the repository

[Aaron Liu]

Srayan Jana said:

Yeah does that dependency include git submodules?

I don't know what that is

[Aaron Liu]

I looked it up and it seems very weird

[Aaron Liu]

you have another repo inside your repo?

[Srayan Jana]

Yes, its a pretty common feature for git repositories.

[Aaron Liu]

I don't know why you would do that for a Lean project

[Srayan Jana]

I'm working on SDL bindings for lean and I need a way to link Lean to SDL's git repo, so I have SDL as a gitsubmodule
https://github.com/oOo0oOo/LeanDoomed/tree/main/vendor

[Aaron Liu]

interesting

[Srayan Jana]

https://github.com/oOo0oOo/LeanDoomed/blob/main/.gitmodules

[Aaron Liu]

I will try to find out if this will affect anything

[Srayan Jana]

@Aaron Liu https://github.com/Ravbug/sdl3-sample/tree/main
here's a C++ project that uses submodules as dependencies, and update the repositories every so often

[Aaron Liu]

I think it clones the repo so whatever that does

[Aaron Liu]

probably relevant
https://github.com/leanprover/lean4/blob/c6abc3c0368e10c49e9762fda1819ad0e95c9bb0/src/lake/Lake/Util/Git.lean#L65-L66
https://github.com/leanprover/lean4/blob/c6abc3c0368e10c49e9762fda1819ad0e95c9bb0/src/lake/Lake/Load/Materialize.lean#L38-L47
https://github.com/leanprover/lean4/blob/c6abc3c0368e10c49e9762fda1819ad0e95c9bb0/src/lake/Lake/DSL/Syntax.lean#L125-L129

[Srayan Jana]

oof it doesnt seem to clone the submodules, thats a big issue.
There should be a command being called that looks something like
git submodule update --init --recursive
https://stackoverflow.com/a/10168693

[Srayan Jana]

it should be called right after git clone is called on the repository

[Anthony Wang]

Aaron Liu said:

I don't know why you would do that for a Lean project

I've seen at least one Lean project with submodules, for instance https://github.com/leanprover/SampCert/blob/main/.gitmodules

[Anthony Wang]

If you clone using git clone --recursive then it will also clone the submodules so you don't have to run that git submodule command manually, but it looks like lake doesn't do that, based on the https://github.com/leanprover/lean4/blob/c6abc3c0368e10c49e9762fda1819ad0e95c9bb0/src/lake/Lake/Util/Git.lean#L65-L66 link that @Aaron Liu sent.

[Srayan Jana]

https://github.com/leanprover/lean4/issues/10467
made an issue, this should be a pretty easy fix/thing to test

[Srayan Jana]

Made a test project to show that it doesn't work: https://github.com/ValorZard/Test-Lean-Git-Submodule
(it doesn't compile for other reasons, but you can see that it never fills out the gits ubmodule in ".lake\packages\SampCert\Tests\IBM"

[Julian Berman]

In the interim switching to subtrees (which are anyhow better :devil: ) is a workaround just in case you haven't considered that.