Questions tagged [installation]
Use this tag for basic setup and installation of theorem prover software.
12 questions
-1
votes
1
answer
71
views
Using Coq after installation [closed]
I have installed Coq from my package manager on ubuntu. How can I run some basic theorem that I can easily understand its proof with Coq.
- 1
1
vote
1
answer
473
views
An installation error in "Mathematics in Lean"
I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message:
...
- 11
-1
votes
2
answers
79
views
Coq makefile complains about extension points on Windows 10
I installed Coq 8.16.1 on Windows 10 recently. I have a full development previously written in Coq 8.9.0 on Linux and want to upgrade to this.
When I run make, I get this error:
...
0
votes
0
answers
148
views
Help with fixing a Coq installation using docker and vscoq
I'm following the logic foundation preface and just began learning. I tried to use the docker with vscoq like the suggested in the book but it didn't work for me and kept asking me to install coq ...
2
votes
1
answer
564
views
How to install dependencies correctly? [Cannot find a physical path bound to logical path]
There's this library I'd like to use. The idea is to be able to use this library with Require Import easily in any other *.v ...
- 143
0
votes
1
answer
244
views
I don't know how to fire up coqtail
I installed coq and coqtail in my computer. According to this page:
https://github.com/whonore/Coqtail
Im now supposed to use the command
CoqStart
to launch the plugin. However, when I type ":...
- 103
4
votes
1
answer
459
views
Error when starting a project in Lean, 'binary package was not provided for 'windows''
after taking a break of half a year I would like to get back to proving things in Lean. I followed the instructions to install a fresh lean project. When I do
...
- 193
2
votes
0
answers
199
views
Cannot open pixbuf loader module file in Windows
I installed Coq from the 8.15 64-bit installation file in Windows. I ran coqide and got the error message:
...
- 43
6
votes
1
answer
793
views
How to install Lean-4 stable only?
I followed Lean documentation to install Lean 4 on my Ubuntu Linux (20.04 LTS) using the elan option described there, and updated it to Lean4 ...
- 2,662
17
votes
3
answers
1k
views
Proof Assistants for Vim Users
I remember the last time I was trying to get into proof assistants, I was discouraged by the lack of functionality for vim users. At the time, it seemed like a lot of powerful features (holes, etc) ...
- 329
61
votes
10
answers
11k
views
Proof assistants for beginners - a comparison
What is a good starting point to learn about proof assistants?
The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS - ...
- 751
8
votes
2
answers
2k
views
How do I install Lean 4?
I want to get started with Lean 4, but I need to install it. The download page links to binaries to download, but I don't know what to do with them. Is there a "best practice" way to install ...
- 238