Questions tagged [installation]
Use this tag for basic setup and installation of theorem prover software.
10
questions
0
votes
0
answers
6
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:
process_begin: ...
0
votes
0
answers
63
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
250
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
115
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
289
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
...
- 183
2
votes
0
answers
138
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:
...
- 23
6
votes
1
answer
438
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 ...
- 1,772
15
votes
3
answers
574
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) ...
- 267
44
votes
9
answers
5k
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 - ...
- 581
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