Updated versions in README; building only cache.

This commit is contained in:
Wen Kokke 2019-07-12 16:01:24 +01:00
parent 2ebe3264a0
commit 124f40c3c2
3 changed files with 6 additions and 9 deletions

View file

@ -38,9 +38,8 @@ before_install:
script: script:
- agda --version - agda --version
- agda2html --version
- acknowledgements --version - acknowledgements --version
- make test-offline # - make test-offline # disable to only build cache
before_deploy: before_deploy:
- acknowledgements -i _config.yml >> _config.yml - acknowledgements -i _config.yml >> _config.yml

View file

@ -5,16 +5,16 @@ permalink: /GettingStarted/
--- ---
[![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io) [![Build Status](https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev)](https://travis-ci.org/plfa/plfa.github.io)
[![Agda](https://img.shields.io/badge/agda-2.5.4.2-blue.svg)](https://github.com/agda/agda/releases/tag/v2.5.4.2) [![Agda](https://img.shields.io/badge/agda-2.6.0.1-blue.svg)](https://github.com/agda/agda/releases/tag/v2.6.0.1)
[![agda-stdlib](https://img.shields.io/badge/agda--stdlib-0.17-blue.svg)](https://github.com/agda/agda-stdlib/releases/tag/v0.17) [![agda-stdlib](https://img.shields.io/badge/agda--stdlib-1.1-blue.svg)](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
# Getting Started with PLFA # Getting Started with PLFA
There are several tools you need to work with PLFA: There are several tools you need to work with PLFA:
- [Agda](https://agda.readthedocs.io/en/v2.5.4.2/getting-started/installation.html) - [Agda](https://agda.readthedocs.io/en/v2.6.0.1/getting-started/installation.html)
- [Agda standard library](https://github.com/agda/agda-stdlib/tree/5819a4dd9c965296224944f05b1481805649bdc2) - [Agda standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1)
For most of the tools, you can simply follow their respective build instructions. For most of the tools, you can simply follow their respective build instructions.
We list the versions of our dependencies on the badges above. We list the versions of our dependencies on the badges above.
@ -26,7 +26,7 @@ or by downloading [the zip archive](https://github.com/plfa/plfa.github.io/archi
git clone https://github.com/plfa/plfa.github.io git clone https://github.com/plfa/plfa.github.io
Finally, we need to let Agda know where to find the standard library. Finally, we need to let Agda know where to find the standard library.
For this, you can follow the instructions [here](https://agda.readthedocs.io/en/v2.5.4.2/tools/package-system.html#example-using-the-standard-library). For this, you can follow the instructions [here](https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library).
It is possible to set up PLFA as an Agda library as well. It is possible to set up PLFA as an Agda library as well.
If you are trying to complete the exercises found in the `tspl` folder, or otherwise want to import modules from the book, you need to do this. If you are trying to complete the exercises found in the `tspl` folder, or otherwise want to import modules from the book, you need to do this.

View file

@ -15,9 +15,7 @@
<div class="trigger"> <div class="trigger">
<a class="page-link" href="{{ "/" | relative_url }}">The Book</a> <a class="page-link" href="{{ "/" | relative_url }}">The Book</a>
<!--!>
<a class="page-link" href="{{ "/Announcements/" | relative_url }}">Announcements</a> <a class="page-link" href="{{ "/Announcements/" | relative_url }}">Announcements</a>
<---->
<a class="page-link" href="{{ "/GettingStarted/" | relative_url }}">Getting Started</a> <a class="page-link" href="{{ "/GettingStarted/" | relative_url }}">Getting Started</a>
<a class="page-link" href="{{ "/Citing/" | relative_url }}">Citing</a> <a class="page-link" href="{{ "/Citing/" | relative_url }}">Citing</a>
<a class="page-link" href="{{ "https://agda-zh.github.io/PLFA-zh/" | relative_url }}">中文</a> <a class="page-link" href="{{ "https://agda-zh.github.io/PLFA-zh/" | relative_url }}">中文</a>