Merge branch 'master' into 637-behavior-of-plutus-v3-scripts-without-…

…datum

CONTRIBUTING.md

@@ -61,6 +61,8 @@ To install Agda locally and use that install with emacs, you can do the followin
 
 `nix-shell` provides Agda complete with the correct dependencies. So you should be able to run your preferred editor within `nix-shell` and it should see the required `agda` executable.
 
+For instructions _not using_ `nix-shell`, check [Setup without nix-shell](setup-without-nix-shell).
+
 ## Working on libraries
 
 To work simultaneously on the ledger and one of its dependencies, the easiest way to do this is to remove the library from the ledger's `.agda-lib` file and add its path to the `include:` section. Then, when finished, push the changes to the library, then update `default.nix` to point to your new commit.
@@ -110,6 +112,33 @@ niv update nixpkgs -r 4e329926df7ee5fa49929a83d31ee7d541f8b45c
 niv update nixpkgs -v 21.11.337905.902d91def1e
 ```
 
+## Setup without nix-shell
+
+- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-1-install-agda>).
+- In a folder `LIB`, clone the dependencies
+    + [agda-stdlib](https://github.com/agda/agda-stdlib)
+    + [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes)
+    + [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta)
+    + [agda-sets](https://github.com/input-output-hk/agda-sets)
+and checkout the commits/tags found in `default.nix` (e.g. `v2.1.1` for `agda-stdlib-meta`).
+- Create a file `LIB/libraries` with the following content:
+```
+LIB/agda-stdlib/standard-library.agda-lib
+LIB/agda-stdlib-classes/agda-stdlib-classes.agda-lib
+LIB/agda-stdlib-meta/agda-stdlib-meta.agda-lib
+LIB/agda-sets/abstract-set-theory.agda-lib
+```
+- Instead of `agda` use `agda --library-file LIB/libraries`. For example, to typecheck `Everything.agda`:
+  ```
+  cd src/
+  agda --library-file LIB/libraries Everything.agda
+  ```
+
+  To build targets from the Makefile (e.g. see [Building other artifacts](building-other-artifacts)), use:
+  ```
+  AGDA="agda --library-file LIB/libraries" make html
+  ```
+
 ## Maintainer
 
 This repository is maintained by @WhatisRT.

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 -- Proof that the rules under Ledger.Conway.Conformance are equivalent
 -- to the rules under Ledger.
 

src/Ledger/Conway/Conformance/Equivalence/Base.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 open import Ledger.Abstract
 open import Ledger.Transaction using (TransactionStructure)

src/Ledger/Conway/Conformance/Equivalence/Bisimilarity.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 module Ledger.Conway.Conformance.Equivalence.Bisimilarity where
 

src/Ledger/Conway/Conformance/Equivalence/Certs.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 open import Ledger.Prelude
 open import Ledger.Abstract

src/Ledger/Conway/Conformance/Equivalence/Convert.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 module Ledger.Conway.Conformance.Equivalence.Convert where
 

src/Ledger/Conway/Conformance/Equivalence/Deposits.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 open import Ledger.Prelude
 open import Ledger.Abstract

src/Ledger/Conway/Conformance/Equivalence/Gov.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --safe #-}
+
 open import Ledger.Prelude
 open import Ledger.Abstract
 open import Ledger.Transaction using (TransactionStructure)

src/Ledger/Conway/Conformance/Equivalence/Map.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --safe #-}
 
 module Ledger.Conway.Conformance.Equivalence.Map where
 

src/Ledger/Conway/Conformance/Equivalence/Utxo.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 open import Ledger.Prelude
 open import Ledger.Abstract

src/Ledger/Enact.lagda

@@ -31,7 +31,7 @@ Note that all other fields of \EnactState also contain a \GovActionID
 since they are \HashProtected.
 
 \begin{figure*}[h]
-\begin{AgdaSuppressSpace}
+\begin{AgdaMultiCode}
 \begin{code}
 record EnactEnv : Type where
 \end{code}
@@ -90,7 +90,7 @@ data
 \begin{code}
   _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Type
 \end{code}
-\end{AgdaSuppressSpace}
+\end{AgdaMultiCode}
 \caption{Types and function used for the ENACT transition system}
 \label{fig:enact-defs}
 \end{figure*}

src/Ledger/Transaction.lagda

@@ -61,7 +61,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 
 \begin{figure*}[h]
 \emph{Abstract types}
-\begin{AgdaMultiCode}
 \begin{code}
         Ix TxId AuxiliaryData : Type
 \end{code}
@@ -110,7 +109,6 @@ Ingredients of the transaction body introduced in the Conway era are the followi
   open GovernanceActions hiding (Vote; yes; no; abstain) public
 
   open import Ledger.Certs govStructure using (DCert)
-
 \end{code}
 \begin{NoConway}
 \emph{Derived types}
@@ -126,6 +124,7 @@ Ingredients of the transaction body introduced in the Conway era are the followi
 \end{code}
 \end{NoConway}
 \emph{Transaction types}
+\begin{AgdaMultiCode}
 \begin{code}
   record TxBody : Type where
 \end{code}