Zulip Chat Archive

Stream: lean4

Topic: unknown package

Kayla Thomas (Jun 04 2023 at 03:43):

Is a workspace different than opening a folder? I'm not sure how to resolve this error message:

unknown package 'Project'
You might need to open '/home/pthomas/Desktop/github/lean4/Fol' as a workspace in your editor

Screenshot-from-2023-06-03-20-39-38.png

Kayla Thomas (Jun 04 2023 at 03:44):

That path is the folder opened in VS Code.

Siddhartha Gadgil (Jun 04 2023 at 04:57):

Does your lakefile.lean list the project? Also you should open the folder so that lakefile.lean is at top level (not the project subfolder).

Kayla Thomas (Jun 04 2023 at 05:03):

How do I list it? I have the default:

import Lake
open Lake DSL

package «fol» {
  -- add any package configuration options here
}

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

@[default_target]
lean_lib «Fol» {
  -- add any library configuration options here
}

Mac Malone (Jun 04 2023 at 11:25):

Based on your directory structure, you should have lean_lib Project instead of lean_lib <<Fol>> and your All.lean should be named Project.lean.

Mac Malone (Jun 04 2023 at 11:27):

@Kayla Thomas However, since your package is named fol, it might be wise to change rename your Project directory Fol and change your imports from Project.* to Fol.*.

Mario Carneiro (Jun 04 2023 at 13:51):

This is an artifact of mathport project oneshot, it always names the output sources Project and you have to use find/replace to rename it to your actual project

Mario Carneiro (Jun 04 2023 at 13:53):

(or set this name in the project config file, which we are not currently suggesting in the readme)

Kayla Thomas (Jun 04 2023 at 18:04):

Thank you.

Filippo A. E. Nuccio (Oct 25 2023 at 11:39):

I don't understand where the problem lies in the following configuration:
image.png

Mauricio Collares (Oct 25 2023 at 11:43):

Does import LocalClassFieldTheory.PadicCompare work?

Filippo A. E. Nuccio (Oct 25 2023 at 11:44):

It requires me to rebuild imports (which I did) and then shows an error:

`c:\Users\nf51454h\.elan\toolchains\leanprover--lean4---v4.2.0-rc4\bin\lake.exe print-paths Init Mathlib LocalClassFieldTheory.PadicCompare` failed:

stderr:
info: [626/3849] Building LocalClassFieldTheory.PadicCompare
error: > LEAN_PATH=.\lake-packages\std\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\Cli\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\build\lib PATH c:\Users\nf51454h\.elan\toolchains\leanprover--lean4---v4.2.0-rc4\bin\lean.exe .\.\.\LocalClassFieldTheory\PadicCompare.lean -R .\.\. -o .\build\lib\LocalClassFieldTheory\PadicCompare.olean -i .\build\lib\LocalClassFieldTheory\PadicCompare.ilean -c .\build\ir\LocalClassFieldTheory\PadicCompare.c
error: stdout:
.\.\.\LocalClassFieldTheory\PadicCompare.lean:1:0: error: unknown package 'DiscreteValuationRing'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:8:0: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:61:5: error: unknown namespace 'IsDedekindDomain'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:66:25: error: unexpected token '('; expected '}'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:74:27: error: invalid binder annotation, type is not a class instance
  ?m.32
use the command `set_option checkBinderAnnotations false` to disable the check
.\.\.\LocalClassFieldTheory\PadicCompare.lean:78:5: error: unknown namespace 'Valuation'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:80:12: error: unknown namespace 'DiscreteValuation'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:82:22: error: unknown constant 'Rat.metricSpace'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:85:28: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:89:18: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:89:18: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:90:3: error: unknown identifier 'pHeightOneIdeal'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:90:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:90:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:92:27: error: unknown constant 'padic_valued'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:98:2: error: unknown identifier 'adicCompletion'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:98:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:97:4: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:100:11: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:100:11: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:101:2: error: unknown identifier 'Completion.isDiscrete'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:101:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:103:11: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:103:11: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:104:2: error: unknown identifier 'RankOneValuation.ValuedField.toNormedField'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:104:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:107:16: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:107:16: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:107:37: error: invalid {...} notation, expected type is not known
.\.\.\LocalClassFieldTheory\PadicCompare.lean:107:37: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:122:5: error: unknown namespace 'NNReal'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:124:12: error: unknown namespace 'Classical'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:126:22: error: unknown constant 'Rat.metricSpace'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:130:18: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:130:18: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:131:3: error: unknown identifier 'pHeightOneIdeal'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:131:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:131:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:133:28: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:136:27: error: unknown constant 'padic_valued'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:141:24: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:177:24: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:192:59: error: unexpected token '['; expected ')'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:222:44: error: unexpected token '['; expected ')'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:227:15: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:227:15: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:227:36: error: invalid {...} notation, expected type is not known
.\.\.\LocalClassFieldTheory\PadicCompare.lean:227:36: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:228:13: error: unexpected token '['; expected command
.\.\.\LocalClassFieldTheory\PadicCompare.lean:239:20: error: unexpected token '+'; expected term
.\.\.\LocalClassFieldTheory\PadicCompare.lean:253:19: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:256:63: error: unexpected token '['; expected ')'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:260:31: error: unexpected token '+'; expected term
.\.\.\LocalClassFieldTheory\PadicCompare.lean:265:33: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:268:60: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:280:22: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:287:11: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:287:11: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:288:3: error: unknown identifier 'padicEquiv'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:288:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:288:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:290:21: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:293:29: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:299:43: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:308:78: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:323:49: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:339:4: error: unknown identifier 'Valued.v'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:339:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:339:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:341:64: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:350:64: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:362:4: error: expected '{' or indented tactic sequence
.\.\.\LocalClassFieldTheory\PadicCompare.lean:371:5: error: unknown tactic
.\.\.\LocalClassFieldTheory\PadicCompare.lean:374:41: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:377:11: error: unknown constant 'CoeFun'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:377:11: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:378:2: error: unknown identifier 'HeightOneSpectrum.valuedAdicCompletion'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:378:2: error: unknown constant 'sorryAx'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:381:51: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:404:5: error: unknown namespace 'Filter'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:406:12: error: unknown namespace 'Filter'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:410:33: error: unexpected token '['; expected ':=', 'where' or '|'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:417:54: error: unexpected token '['; expected ')'
.\.\.\LocalClassFieldTheory\PadicCompare.lean:439:76: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:469:6: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:498:6: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:527:60: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:550:73: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:573:43: error: expected token
.\.\.\LocalClassFieldTheory\PadicCompare.lean:577:49: error: expected token
error: external command `c:\Users\nf51454h\.elan\toolchains\leanprover--lean4---v4.2.0-rc4\bin\lean.exe` exited with code 1

Filippo A. E. Nuccio (Oct 25 2023 at 11:44):

I should probably also add my lakefile.lean, which is as follows:

import Lake
open Lake DSL

package «LocalClassFieldTheory» {
  -- add any package configuration options here
}

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

@[default_target]
lean_lib «LocalClassFieldTheory» {
  -- add any library configuration options here
}

Mauricio Collares (Oct 25 2023 at 11:48):

The errors above mean the relevant imports in PadicCompare.lean also need to be updated to start with LocalClassFieldTheory. (and transitive imports as well)

Filippo A. E. Nuccio (Oct 25 2023 at 11:50):

OK, let me try

Filippo A. E. Nuccio (Oct 25 2023 at 11:51):

But I thought that the line @[default_target] was made to avoid this, no?

Mauricio Collares (Oct 25 2023 at 11:51):

I think that line just means you can type lake build instead of lake build LocalClassFieldTheory, but I'm not sure

Last updated: Dec 20 2023 at 11:08 UTC