readme updates

README.md

@@ -1,17 +1,31 @@
-
-# On the Expressive Power of Variability Languages
+# On the Expressive Power of Languages for Static Variability
 
 [![agda][agda-badge-version-svg]][agda-badge-version-url]
 
-This is the supplementary Agda library for our paper _On the Expressive Power of Variability Languages_ submitted to Object-Oriented Programming, Systems, Languages, and Applications 2024 (in PACM PL) (OOPSLA 2024). 
+This is the supplementary Agda library for our paper _On the Expressive Power of Languages for Static Variability_ submitted to Object-Oriented Programming, Systems, Languages & Applications 2024 (OOPSLA 2024). 
 
 ## Setup
 
-The library needs Agda version 2.6.3 (newer version should also work but we did not test them). We tested our setup on Ubuntu (inside windows subsystem for linux (WSL 2)) and Manjaro. The only dependency of this library is the Agda standard library which is shipped as a git submodule within the `agda-stdlib` directory (already contained within the zip file of the supplementary material).
+The library needs Agda version 2.6.3 (newer version should also work but we did not test them). We tested our setup on Ubuntu (inside windows subsystem for linux (WSL 2)), Manjaro, and NixOS. The only dependency of this library is the Agda standard library which is shipped as a git submodule within the `agda-stdlib` directory (already contained within the zip file of the supplementary material).
 
 ### Installation
 
-To compile the library and run its small demo, you need to have Agda installed.
+There are two ways to compile the library and run its small demo.
+Either use Nix, or install Agda manually.
+We recommend using Nix.
+
+#### Installation via Nix
+
+When you have Nix installed on your system, navigate to this directory and then simply open a nix shell
+``` shell
+nix-shell
+```
+or alternatively, run the demo directly
+``` shell
+nix-build
+```
+
+#### Manual Installation
 We recommend following the installation instructions from the [Programming Language Foundations in Agda](https://plfa.github.io/GettingStarted/) book to install GHC, Cabal, and Agda (no need to install the book and the standard-library, which is shipped in the right version in the subdirectory `agda-stdlib` here).
 
 TL;DR: In summary, when following the book, you have to do:
@@ -40,7 +54,7 @@ TL;DR: In summary, when following the book, you have to do:
 
 Detailed installation instructions can also be found [in the official documentation](https://agda.readthedocs.io/en/v2.6.3/getting-started/installation.html), too.
 
-3. Finding the standard library: Agda looks for its dependencies in a directory specified by the environment variable `AGDA_DIR`. The provided makefile sets this environment variable during the build process to the `.libs` directory within this repository. If you want to run `agda` manually, or if you want to work on this project in an editor (e.g., emacs) then you have to set this environment variable to the libs directory in this repository.
+3. Finding the standard library: Agda looks for its dependencies in a directory specified by the environment variable `AGDA_DIR`. The provided makefile sets this environment variable temporarily, and locally during the build process to the `.libs` directory within this repository. (Your global setup will not be affected). If you want to run `agda` manually, or if you want to work on this project in an editor (e.g., emacs) then you have to set this environment variable to the libs directory in this repository.
 
     ```shell
     export AGDA_DIR="path/to/this/repository/libs"
@@ -54,22 +68,30 @@ To test whether you setup Agda correctly, and to run this libraries demo, run ma
 ```shell
 make
 ```
-which will compile the library and run its small demo.
+which will compile the library and run its small demo. Alternatively, you may use `nix-build` as explained above.
+
+Building for the first time will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min). Running the demo will print:
+
+- some translations of core to binary choice calculus, and
+- some translations from option calculus to binary choice calculus, and
+- some examples of feature structure tree composition.
 
-Building for the first time will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min). Running the demo will print some translations of core to binary choice calculus, and translations from option calculus to binary choice calculus. When running the demo, make sure your terminal is in full-screen because the demo assumes to have at least 100 characters of horizontal space in the terminal for pretty-printing.
+When running the demo, make sure your terminal is in full-screen because the demo assumes to have at least 100 characters of horizontal space in the terminal for pretty-printing.
+Also, the demo prints unicode characters to terminal, which should be supported.
+There will be a short hint at the beginning of the demo with some test characters.
 
 ## Project Structure
 
 The library is organized as follows:
 
-- [src/Framework](src/Framework) contains the definitions of our formal framework, defined in Section 4 in our paper.
-  Here, you can find the core data types in [Definitions.lagda.md](src/Framework/Definitions.lagda.md).
-  Soundness and completeness are defined in the [Properties](src/Framework/Properties) sub-directory.
-  Definitions for expressiveness and other relations are in the [Relation](src/Framework/Relation) sub-directory.
-  Theorems for proving completeness, soundness, and expressiveness based on their relationships (Section 4.5) are within the [Proof](src/Framework/Proof) sub-directory.
-- [src/Lang](src/Lang) contains instantiations of particular variability languages.
-- [src/Translation](src/Translation) contains translations between variability languages, such as the translation of option calculus to binary choice calculus in [OC-to-2CC.lagda.md](src/Translation/OC-to-2CC.lagda.md) (Section 5.3 in our paper).
-- [src/Test](src/Test) contains definitions of unit tests for translations and some experiments that are run, when running the library.
+- The [src/Framework](src/Framework) directory contains the definitions of our formal framework, defined in Section 4 in our paper.
+  - [VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md) defines variability languages and their denotational semantics.
+  - Soundness and completeness are defined in the [Properties](src/Framework/Properties) sub-directory.
+  - Definitions for expressiveness and configuration equivalence are in the [Relation](src/Framework/Relation) sub-directory.
+  - Theorems for proofs for free (Section 4.4) are within the [Proof](src/Framework/Proof) sub-directory, including several more interesting theorems, which did not fit into the paper.
+- [src/Lang](src/Lang) contains definitions of particular variability languages (Section 3).
+- [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) contains an overview of our case study (Section 5) to compare existing variability languages. The compilers can be found in the [src/Translation/Lang](src/Translation/Lang) sub-directory.
+- [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) implements the theory of indexed sets with various operators and equational reasoning.
 
 [agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.3-blue.svg
 [agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.6.3