Skip to main content

Questions tagged [installation]

Use this tag for basic setup and installation of theorem prover software.

Filter by
Sorted by
Tagged with
-1 votes
1 answer

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.
Djoser's user avatar
  • 1
0 votes
1 answer

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: ...
Blankino's user avatar
-1 votes
2 answers

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: ...
Daniel Bee's user avatar
0 votes
0 answers

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 ...
Abde Mojito's user avatar
2 votes
1 answer

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 ...
Julián's user avatar
  • 143
0 votes
1 answer

I don't know how to fire up coqtail

I installed coq and coqtail in my computer. According to this page: Im now supposed to use the command CoqStart to launch the plugin. However, when I type ":...
Raul Gomez's user avatar
4 votes
1 answer

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 ...
Strichcoder's user avatar
2 votes
0 answers

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: ...
Moti's user avatar
  • 23
6 votes
1 answer

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 ...
tinlyx's user avatar
  • 2,034
17 votes
3 answers

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) ...
Chris Grossack's user avatar
56 votes
10 answers

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 - ...
Piotr Migdal's user avatar
8 votes
2 answers

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 ...
pxeger's user avatar
  • 238