Comments (3)
jcommelin
commented on August 16, 2024
@dbonattoj Did you properly open the tutorials folder as a "VScode project"? If not, I hope that solves your problem. If you did, then I don't know an immediate solution. Maybe we can debug it over at https://leanprover.zulipchat.com/
from mathlib-tools.
dbonattoj
commented on August 16, 2024
Thanks!! It seems to work normally by opening a folder instead of appending a folder to the current workspace, but I don't get why..
Usually, I open several folders in the same workspace without any issues (python projects), Here, I had 2-3 lean projects opened at the same time in the workspace using "file>Add Folder to Workspace"
Complete procedure:
leanproject get tutorials
cd tutorials
leanproject.exe build
Open an empty VS Code and reach the menu "Open Folder".
from mathlib-tools.
bryangingechen
commented on August 16, 2024
I don't think we have support for multiple directories in a workspace in the vscode-lean extension right now.
from mathlib-tools.
Related Issues (20)
- Missing / inconsistent version tags HOT 1
- macOS installer should suggest install steps for M1 users HOT 3
- Make a longest-pole script HOT 1
- 'leanproject new' fails with lean 4 installed HOT 2
- `toml` to `tomli` & `tomli_w` migration HOT 6
- [email protected] has a dependency on numpy, but pip doesn't install it automatically HOT 6
- import-graph dot file HOT 1
- clean up git after leanproject get-mathlib-cache HOT 5
- permissions problems with `leanproject up` on Windows HOT 3
- Interrupting download leaves corrupted archive behind HOT 1
- Support looking for leanpkg.toml in cwd HOT 1
- failure with old project
- leanproject get-mathlib-cache doesn't tidy up after itself HOT 1
- SSH problems HOT 5
- leanproject hooks scripts are out of date HOT 2
- refactoring directory structure of mathlib can cause problems HOT 1
- mathlib get-cache and similar should support fetching at specified hash HOT 1
- `elan` is not on $PATH in gnome-terminal HOT 2
- why are we still talking about branch 'lean-3.4.2'? HOT 3
- MacOS brew update of Python breaks leanproject HOT 7
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from mathlib-tools.