Add PLFA/src/plfa.agda-lib to AGDA_DIR/libraries and add plfa to AGDA_DIR/defaults, each on a line of their own. To do so, let PLFA be the path to the root directory for PLFA. If you want to complete the exercises or to import modules from the book, you will also need to provide access to PLFA as an Agda library.In AGDA_DIR, create a plain-text file called defaults containing just the line standard-library.This lets Agda know that an Agda library called standard-library is available. In AGDA_DIR, create a plain-text file called libraries containing AGDA_STDLIB/standard-library.agda-lib, where AGDA_STDLIB is the path to where the Agda standard library is located (e.g., ~/plfa/standard-library/).If the AGDA_DIR directory does not already exist, create it.
On Windows, AGDA_DIR usually defaults to %AppData%\agda, where %AppData% usually defaults to C:\Users\USERNAME\AppData\Roaming. On UNIX and macOS, AGDA_DIR defaults to ~/.agda. Both configuration files are located in the directory AGDA_DIR. Otherwise, you will need to edit the appropriate files. This provides access to both the Agda standard library and to PLFA as an Agda library. Mkdir -p ~/.agda cp ~/plfa/data/dotagda/ * ~/.agda For most versions of macOS, you can install these by running the following command: On macOS, you’ll need to install The XCode Command Line Tools. On macOS: Install the XCode Command Line Tools Therefore, it’s important to have the specific versions of Agda and the standard library shown above. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. There are several versions of Agda and its standard library online. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems. PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. However, if you wish to interact with the code or complete the exercises, you need several things: Emacs Org Mode: (see ) Make sure org mode is loaded! ( message "Adding Org Mode to path." ) ( setq load-path ( cons "~/pkg/emacs/org-7.01h/lisp" load-path )) ( setq load-path ( cons "~/pkg/emacs/org-7.01h/contrib/lisp" load-path )) Log when tasks are completed ( setq org-log-done t ) To save clock history across Emacs sessions: ( setq org-clock-persist 'history ) ( org-clock-persistence-insinuate ) To add a note when you clock out: ( setq org-log-note-clock-out t ) use CDLaTeX to enter math ( setq load-path ( cons "~/pkg/emacs" load-path )) ( add-hook 'org-mode-hook 'turn-on-org-cdlatex ) Start emacs in ~/org (setq default-directory "~/org") Start emacs in org mode ( org-mode )Īnother module I use is called icicles, it provides pre-loaded tab-completion that I can move through with arrow-up or arrow-down.You can read PLFA online without installing anything. To build from source, you can build a command-line-only emacs using this configure line: This also allows you to customize it as you see fit, which is appropriate, since emacs is famous for being the world's most customizable text editor.
I highly recommend Aquamacs for Mac users, but if you're looking for a more universal emacs experience (one that won't leave you confused and looking up keyboard shortcuts when you have to use emacs remotely on a *nix terminal), I would highly recommend building emacs from source.
0 kommentar(er)
