All Projects → Ptival → Peacoq

Ptival / Peacoq

Licence: mit
PeaCoq is a pretty Coq, isn't it?

Labels

Projects that are alternatives of or similar to Peacoq

Poleiro
A blog about Coq
Stars: ✭ 42 (-57.58%)
Mutual labels:  coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (-34.34%)
Mutual labels:  coq
Typetheory
The mathematical study of type theories, in univalent foundations
Stars: ✭ 86 (-13.13%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-48.48%)
Mutual labels:  coq
Collapsing Towers
Collapsing Towers of Interpreters
Stars: ✭ 61 (-38.38%)
Mutual labels:  coq
Certicoq
A Verified Compiler for Gallina, Written in Gallina
Stars: ✭ 66 (-33.33%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-58.59%)
Mutual labels:  coq
Coq Serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Stars: ✭ 87 (-12.12%)
Mutual labels:  coq
Riscv Coq
RISC-V Specification in Coq
Stars: ✭ 63 (-36.36%)
Mutual labels:  coq
Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (-14.14%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-47.47%)
Mutual labels:  coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-39.39%)
Mutual labels:  coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-25.25%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-52.53%)
Mutual labels:  coq
Vscoq
Coq Support for Visual Studio Code
Stars: ✭ 85 (-14.14%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-57.58%)
Mutual labels:  coq
Sfja
SoftwareFoundations(Ja)
Stars: ✭ 65 (-34.34%)
Mutual labels:  coq
Ttlite
A SuperCompiler for Martin-Löf's Type Theory
Stars: ✭ 94 (-5.05%)
Mutual labels:  coq
Fourcolor
Formal proof of the Four Color Theorem
Stars: ✭ 87 (-12.12%)
Mutual labels:  coq
Ch2o
Stars: ✭ 75 (-24.24%)
Mutual labels:  coq

PeaCoq logo PeaCoq

Build Status

Docker Hub

Getting ready (everyone)

$ git clone https://github.com/Ptival/PeaCoq.git
$ cd PeaCoq

Dependencies (NixOS)

For all of you 1337 hax0rz, shell.nix should pull all the necessary dependencies.

$ nix-shell
# brace yourself, this might take a while the first time!

Dependencies (other distributions)

Using your package manager of choice, pull the following dependencies:

Dependency Version Bound Comment
cabal-install 1.22 ~ Use the most recent available
Camlp5 6.14 ? Not sure, just get the most recent available
Coq 8.5 + Will definitely not work on < 8.5
GHC 7.10.2 ~+ I believe I use some of the recent features
NodeJS (npm) 3.8.6 ? Any version might work
OCaml 4.02.3 ~+ Might work on anything >= 4, if Coq builds

Plus, the following cabal dependencies must be pulled manually:

$ cabal install alex happy

Building (everyone)

Optionally (but recommended), you can run cabal update, then:

$ ./setup.sh

setup.sh will perform a lot of operations:

  1. Check that the required software is present and versions

  2. Clean up existing installations of peacoqtop and peacoq-server

  3. Build and install peacoqtop, a wrapper around coqtop

  4. Build and install peacoq-server, a small server to communicate with the front-end

  5. make the OCaml plugin that enriches Coq's protocol for PeaCoq

  6. npm install some JavaScript modules needed by the front-end

  7. typings install some TypeScript definitions needed to type-check the front-end

  8. tsc -p . transpiles the front-end from TypeScript to JavaScript

  9. Finally a configuration file will be created in your home directory

So it will take a while the first time, and steps 3, 4, 6, and 7 will require an Internet connection.

Running PeaCoq

./peacoq -p <PORT>

Then navigate to http://localhost:<PORT>/index.html to start using PeaCoq!

Shortcuts

<C> will refer to a Ctrl or Command key. <M> will refer to a Alt or Option key.

Note: certain shortcuts offer a poor user experience on Windows and possibly MacOS.

They will eventually be re-bind-able. Feel free to alter them in web/ts/editor/keybindings.ts.

Shortcut Action
<C> <M> L Load a file
<C> <M> S Save a file
<C> <M> Up Step backward
<C> <M> Right Step to caret
<C> <M> Down Step forward
<C> <M> + Increase font
<C> <M> - Decrease font
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].