Skip to content

Commit

Permalink
Merge pull request formal-land#199 from foobar-land/update-links
Browse files Browse the repository at this point in the history
Update the documentation links to foobar-land.github.io
  • Loading branch information
clarus authored Oct 15, 2021
2 parents c9c86b0 + 5c2e073 commit 53ea6b8
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 7 deletions.
8 changes: 4 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# ![Logo](https://clarus.github.io/coq-of-ocaml/img/rooster-48.png) coq-of-ocaml [![CI](https://github.com/clarus/coq-of-ocaml/workflows/CI/badge.svg?branch=master)](https://github.com/clarus/coq-of-ocaml/actions?query=workflow%3ACI)
# ![Logo](https://foobar-land.github.io/coq-of-ocaml/img/rooster-48.png) coq-of-ocaml [![CI](https://github.com/clarus/coq-of-ocaml/workflows/CI/badge.svg?branch=master)](https://github.com/clarus/coq-of-ocaml/actions?query=workflow%3ACI)
> Import OCaml programs to Coq for formal verification
**Documentation on https://clarus.github.io/coq-of-ocaml/**
**Documentation on https://foobar-land.github.io/coq-of-ocaml/**

## Aim
`coq-of-ocaml` aims to enable formal verification of [OCaml](https://ocaml.org/) programs 🦄. *The more you prove, the happier you are.* By transforming OCaml code into similar [Coq](https://coq.inria.fr/) programs, it is possible to prove arbitrarily complex properties using the existing power of Coq. The sweet spot of `coq-of-ocaml` is purely functional and monadic programs. Side-effects outside of a monad, like references, and advanced features like object-oriented programming, may never be supported. By sticking to the supported subset of OCaml, you should be able to import millions of lines of code to Coq and write proofs at large. Running `coq-of-ocaml` after each code change, you can make sure that your proofs are still valid. The generated Coq code is designed to be stable, with no generated variable names for example. We recommend organizing your proof files as you would organize your unit-test files.
Expand Down Expand Up @@ -81,10 +81,10 @@ The basic command is:
```
coq-of-ocaml file.ml
```
You can start to experiment with the test files in `tests/` or look at our [online examples](https://clarus.github.io/coq-of-ocaml/examples/). `coq-of-ocaml` compiles the `.ml` or `.mli` files using [Merlin](https://github.com/ocaml/merlin) to understand the dependencies of a project. One first needs to have a **compiled project** with a working configuration of Merlin. This is automatically the case if you use [dune](https://dune.build/) as a build system.
You can start to experiment with the test files in `tests/` or look at our [online examples](https://foobar-land.github.io/coq-of-ocaml/examples/). `coq-of-ocaml` compiles the `.ml` or `.mli` files using [Merlin](https://github.com/ocaml/merlin) to understand the dependencies of a project. One first needs to have a **compiled project** with a working configuration of Merlin. This is automatically the case if you use [dune](https://dune.build/) as a build system.

## Documentation
You can read the documentation on the website of the project at [https://clarus.github.io/coq-of-ocaml/](https://clarus.github.io/coq-of-ocaml/).
You can read the documentation on the website of the project at [https://foobar-land.github.io/coq-of-ocaml/](https://foobar-land.github.io/coq-of-ocaml/).

## Supported
* the core of OCaml (functions, let bindings, pattern-matching,...) ✔️
Expand Down
2 changes: 1 addition & 1 deletion doc/docs/examples.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ title: Examples
The main project handled with `coq-of-ocaml` is the crypto-currency [Tezos](https://tezos.com/). The result is in the project:
* `coq-tezos-of-ocaml`: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/

providing a translation in Coq of the economic protocol of Tezos. You can also look at the [historical result](https://clarus.github.io/coq-of-ocaml/examples/tezos/) of the first compiling translation of the protocol of Tezos.
providing a translation in Coq of the economic protocol of Tezos. You can also look at the [historical result](https://foobar-land.github.io/coq-of-ocaml/examples/tezos/) of the first compiling translation of the protocol of Tezos.

We are now focusing on:
* maintaining the translation of the protocol of Tezos, as the protocol evolves;
Expand Down
2 changes: 1 addition & 1 deletion doc/docs/roadmap.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ title: Future
We present some of the things we have done, and what we could do in the future.

## Done
Our main achievement is the translation of the economic protocol (kernel) of the [Tezos crypto-currency](https://tezos.com/) to a valid [Coq](https://coq.inria.fr/) program. We present the results on our [example page](https://clarus.github.io/coq-of-ocaml/examples/tezos/). This amounts to the translation of around 40.000 lines of [OCaml](https://ocaml.org/), including the definition of interfaces.
Our main achievement is the translation of the economic protocol (kernel) of the [Tezos crypto-currency](https://tezos.com/) to a valid [Coq](https://coq.inria.fr/) program. We present the results on our [example page](https://foobar-land.github.io/coq-of-ocaml/examples/tezos/). This amounts to the translation of around 40.000 lines of [OCaml](https://ocaml.org/), including the definition of interfaces.

## coq-of-ocaml as a kit
Here are some of the tasks that we could do, with an estimated cost in days:
Expand Down
2 changes: 1 addition & 1 deletion doc/website/siteConfig.js
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ const baseUrl = '/coq-of-ocaml/';
const siteConfig = {
title: 'coq-of-ocaml', // Title for your website.
tagline: 'Import OCaml programs to Coq',
url: 'https://clarus.github.io', // Your website URL
url: 'https://foobar-land.github.io', // Your website URL
baseUrl, // Base URL for your project */
// For github.io type URLs, you would set the url and baseUrl like:
// url: 'https://facebook.github.io',
Expand Down

0 comments on commit 53ea6b8

Please sign in to comment.