Error importing files

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone I asked here how to import my own lean files and I managed it to work based on the answers there, but now I've moved to another computer, I've tried to organize everything in a better way and I'm getting an error with the imports.

Here is my explorer and the error I'm getting:

imagen.png

In the file Lemmas.lean I have an import to Defs (import FunctionalAnalysis.MazurTheorem.Defs) and another one to Nets (import Topology.Nets.Nets) and it works fine. What's the problem here?

This is the lakefile:

import Lake
open Lake DSL

package «Projects» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

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

@[default_target]
lean_lib «FunctionalAnalysis» where

@[default_target]
lean_lib «Topology» where

@[default_target]
lean_lib «Aprendizaje» where

Thanks in advance

[Kevin Buzzard]

Judging by the error, your file FunctionalAnalysis/MazurTheorem/Lemmas.lean might have import Nets.something (edit: looks like I was wrong) but your lakefile has no mention of a module called Nets. Maybe post the beginning of Lemmas.lean?

[Esteban Martínez Vañó]

Of course. This is the beggining of Lemmas.lean

imagen.png

[Kim Morrison]

Could you share the repository URL?

[Kim Morrison]

It's very hard to diagnose screen shots.

[Kevin Buzzard]

Is more than one default_target allowed in a lakefile? I have no idea where to look up this sort of thing.

[Esteban Martínez Vañó]

Hi.

Well, that was another thing I wanted to ask here. How can I sincronize lean projects in VCS with Github? Because I've never used Github and I cannot find information about it (I just know that I have git installed because it was recommended in the installation guide).

Anyway, I can try and upload here the relevant files.

Projects.rar

In the rar is the whole folder except for the .lake folder.

If you let me know how can I create the repository I will upload it, of course.

[Matthew Ballard]

Kevin Buzzard said:

Is more than one default_target allowed in a lakefile? I have no idea where to look up this sort of thing.

https://github.com/leanprover/lean4/blob/master/src/lake/README.md#defining-build-targets

[Kevin Buzzard]

You don't need to ask here about how to set up a github repo, you can just google for that (this has nothing to do with Lean). Make an account, make a new repository on github, and then follow the instructions on github and/or the internet about how to upload your local lean project to that repository.

[Esteban Martínez Vañó]

I'll do it the moment I can :+1:

[Esteban Martínez Vañó]

Sorry, I've been out of town and I didn't have access to my computer until today.

Kim Morrison ha dicho:

Could you share the repository URL?

I think I've managed to do it:

https://github.com/Eparoh/Projects

Is it enough to get a better understanding of the error I get?

[Esteban Martínez Vañó]

An error that, by the way, now has magically disappeared and with it the "green colour" on a file when everything was correct.

I mean, if you see this capture:

Esteban Martínez Vañó ha dicho:

Of course. This is the beggining of Lemmas.lean

imagen.png

Archives without errors appear in green and the ones with errors appear in red, but now the "green" is missing (but not the red for errors or the yellow for sorrys):

imagen.png

[Sebastian Ullrich]

Green means "file not tracked in git"