• Stars
    star
    106
  • Rank 325,871 (Top 7 %)
  • Language Coq
  • License
    MIT License
  • Created over 10 years ago
  • Updated over 3 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

PeaCoq is a pretty Coq, isn't it?

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

More Repositories

1

ocamelf

ELF-parsing library written in OCaml for OCaml
OCaml
12
star
2

language-ocaml

Language tools for manipulating OCaml programs in Haskell (parser, pretty-printer, ...)
Haskell
12
star
3

yugioh

Yu-Gi-Oh! simulator
Haskell
10
star
4

chick

Haskell
9
star
5

mock-haskell-projects

A collection of mock Haskell project setups that ought to load properly
8
star
6

lyah-fr

French translation of Learn You A Haskell For Great Good
CSS
8
star
7

recursion-schemes-examples

Examples of using the recursion-schemes package
Haskell
7
star
8

language-coq

Haskell
6
star
9

HaysTac

A pile of Ltac tactics that might contain the needle you're looking for...
Coq
5
star
10

galois

Reproducible setup for Galois
Nix
5
star
11

ProofIDE

Editing proofs made nicer
Haskell
5
star
12

extensible-nanopass-compiler

A Coq implementation of a nanopass compiler, using "Meta-Theory Γ  la Carte" techniques
Coq
4
star
13

social_scrapper

This project contains Scrapy spiders able to crawl some charity/general interest/humanitarian websites to extract data about volunteering opportunities.
Python
4
star
14

yokoiboy

Toy GameBoy emulator, in Rust
Rust
3
star
15

rocq-gameboy

Coq
3
star
16

00-lambda

Starter code for 00-lambda
Haskell
2
star
17

generic-spot-the-difference

Nix
2
star
18

haskell-nix-template

Template for Haskell project using nix + haskell.nix + niv + hpack + haskell-language-server
Nix
2
star
19

peacoqtop

Haskell
2
star
20

peacoq-server

Haskell
2
star
21

learn-from-peers-rxjs

JavaScript
2
star
22

ynot

Harvard's Ynot: http://ynot.cs.harvard.edu/ - One branch per Coq version which needed changes
Coq
2
star
23

advent-of-code

Haskell
1
star
24

coq-of-s2n

1
star
25

lambda-forall

HTML
1
star
26

compcert-alias

Alias analysis for CompCert
Coq
1
star
27

formal

Formalization of some dependently-typed languages
Makefile
1
star
28

peacoq-frontend

PureScript
1
star
29

segfaulty

Nix + Haskell + Polysemy + HIE = GHC panic
Nix
1
star