Skip to content

Commit

Permalink
Updating README and Duper version
Browse files Browse the repository at this point in the history
  • Loading branch information
JOSHCLUNE committed Dec 16, 2023
1 parent 9f2191b commit 1d43df3
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 6 deletions.
6 changes: 5 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,11 @@ This is a sample project that imports both Duper and Mathlib so that users can e

### With VSCode

To build this project with VSCode directly, first make sure that the Lean 4 [VSCode extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) is installed and enabled. Then, on the VSCode welcome page, choose "Clone Git repository" and paste [this](https://github.com/JOSHCLUNE/DuperDemo) url. You will likely see a variety of prompts, potentially asking you to install Lean, rebuild imports, or restart the Lean server. Click the blue buttons on each of them and VSCode will build this project. Note that the first time this project is opened, it may take a couple of minutes to build, though the process should proceed much more quickly after it has successfully been built once.
To build this project with VSCode directly, first make sure that the Lean 4 [VSCode extension](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) is installed and enabled. Then, on the VSCode welcome page, choose "Clone Git repository" and paste [this](https://github.com/JOSHCLUNE/DuperDemo) url. If you do not see "Clone Git repository" on the welcome page, you can also use Ctrl-Shift-P or Command-Shift-P to open the VSCode command palette and enter the command "Git: Clone".

After this project has been cloned, navigate to the project's root directory (the directory that contains this README.md file) and run `lake exe cache get`. Once this command is done running, open DuperDemo.lean in VSCode.

After you open DuperDemo.lean, you will likely see a variety of prompts, potentially asking you to install Lean, rebuild imports, or restart the Lean server. Click the blue buttons on each of them and VSCode will build this project. Note that the first time this project is opened, it may take a couple of minutes to build, though the process should proceed much more quickly after it has successfully been built once.

### With the command line

Expand Down
8 changes: 4 additions & 4 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@
{"git":
{"url": "https://github.com/leanprover-community/duper.git",
"subDir?": null,
"rev": "62754d46df33b0ef562c250141d5b66201a93a60",
"rev": "ab199717883159b2f65a0c120829dafb2695dbda",
"opts": {},
"name": "Duper",
"inputRev?": "v0.0.2",
"inputRev?": "v0.0.3",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4",
Expand Down Expand Up @@ -60,9 +60,9 @@
{"git":
{"url": "https://github.com/leanprover-community/lean-auto.git",
"subDir?": null,
"rev": "00e49cfb3e9a6ced65200c039020ecd053744011",
"rev": "c42a69000568fbadd8bc5664ed22b64b7ff96a62",
"opts": {},
"name": "auto",
"inputRev?": "main",
"inputRev?": "v0.0.2",
"inherited": true}}],
"name": "duperDemo"}
2 changes: 1 addition & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ package «duperDemo» {

require «mathlib» from git "https://github.com/leanprover-community/mathlib4" @ "4e5518cafc0efd7c7b7d287fa960fce5201908db"

require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v0.0.2"
require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v0.0.3"

@[default_target]
lean_lib «duperDemo» {
Expand Down

0 comments on commit 1d43df3

Please sign in to comment.