Working with multiple files

Stream: lean4

[Tomáš Pecl]

Hello. I am using lean4 installed by lean4 extension in VSCode. I opened a folder with VSCode and made a file and written some stuff in it. The interactive panel showed no errors. Then I decided that I want to use multiple files. So I made another file next to the first one. Then I put "import file2" at the beggining of file1. Now the interactive panel is showing an error "unknown package 'file2'". How do I make this work?

[Scott Morrison]

lake new myproject

[Shreyas Srinivas]

For multi-file projects see an example here: https://lean-lang.org/functional_programming_in_lean/hello-world/starting-a-project.html

[Shreyas Srinivas]

In particular for a module Mod1 there is a file called Mod1.lean and a folder called Mod1 contains its submodules.

[Tomáš Pecl]

isnt this for executables? I am doing math proofs.

[Notification Bot]

A message was moved here from #lean4 > wasm build by Tomáš Pecl.

[Shreyas Srinivas]

Tomáš Pecl said:

isnt this for executables? I am doing math proofs.

The module structure doesn't change either way. For math projects see the instructions: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Mauricio Collares]

Then you can create an empty project with lake new ProjectName math, which starts from a template which already includes mathlib and is geared towards theorem proving. Creating a project is important to use multiple files.

[Tomáš Pecl]

ok I am going to try this

[Tomáš Pecl]

Ok it seems like its working. I can probably deal with it now. Thanks