Ferros Specifications

A repository containing specifications and proofs about Ferros.

Rendered Specifications

Installation

NB: The author assumes you’re using Emacs to hack on Agda things.

While what it means to “install” ferros-spec is ambiguous, to use it—that is, to open it and make C-c C-l happy—you’ll first need a functional installation of Agda.

Installing Agda

Install Stack.

$ curl -sSL https://get.haskellstack.org/ | sh

Clone the Agda source.

$ git clone git@github.com:agda/agda.git

Use Stack to build and install Agda.

$ cd agda
$ stack --stack-yaml stack-8.6.4.yaml install

You should see a few lines stating that two binaries were installed agda and agda-mode. agda-mode is the Emacs integration. To hook Agda up to Emacs, run that command and tell it to set itself up.
```
$ agda-mode setup
    
```
If this is not your first go around with an Agda installation, use compile rather than setup. This does the elisp complilation with the fresh source code, but doesn’t touch your init.el file again.

/NB: It will not work if you’ve already run setup to do it again after an update. The first thing that setup does is check your init.el file for the presence of an Agda config. If it’s already there, it does nothing./

Configuring Agda

Agda’s “library system” is… weird, in that it doesn’t really have one. What it does have, is a collection of text files which help the compiler find the right source files. Here’s what you need.

`$AGDA_DIR`

By default, it’s ~/.agda:

The AGDA_DIR defaults to ~/.agda on unix-like systems[.]

The Agda docs

Just leave it there. Don’t rock the boat. I’m fairly sure that this one in particular will capsize.

$AGDA_DIR should contain the following files:

$ tree ~/.agda
/home/dpitt/.agda
├── defaults
└── libraries

2. Libraries

libraries registers Agda libraries through a path to an Agda library file. Ferros has a library file called ferros.agda-lib which you can take a look at if you’d like an example, or you can read more here.

Inside libraries you should add a path to Ferros’s library file:

$ cat ~/.agda/libraries
/home/dpitt/src/ferros-spec/ferros.agda-lib

3. Defaults

defaults contains registered library names which you would like to be loaded any time you open an Agda file. Let’s get setup with the Agda std-lib for an example.

Clone agda-stdlib. I’m keeping the standard library in my ~/.agda folder.

$ git clone git@github.com:agda/agda-stdlib.git ~/.agda/agda-stdlib

$ echo "/home/dpitt/.agda/agda-stdlib/standard-library.agda-lib" >> ~/.agda/libraries

Include it in defaults.

$ echo standard-library >> ~/.agda/defaults

Now modules from the standard library can be imported any time you open an Agda file.

Latex

There exists files in the spec which are literate Agda files, in particular those that contain the types we wish to prove certain properties about. PDFs can be generated from those files by using the latex make directive:

$ make latex

When this command completes, you will find PDFs which correspond to those Agda files in the pdf directory.

License

See LICENSE for more details.

Licensed under the Apache License, Version 2.0 (the “License”); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an “AS IS” BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

auxoncorp/ferros-spec