Vatras is the supplementary Agda library for our OOPSLA'24 paper:

On the Expressive Power of Languages for Static Variability. Paul M. Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw, Parisa Ataei, Thomas Thüm. Object-Oriented Programming, Systems, Languages & Applications, 2024 (OOPSLA 2024).

This library formalizes all results in our paper:

• All formal languages for static software variability presented in our survey (Section 3 Table 1) are formalized as algebraic datatypes.
• The library implements our formal framework for language comparisons, including necessary data structures, theorems, and proofs (Section 4).
• This library contains all theorems and proofs to establish the map of variability languages we find by comparing the languages from our survey with our framework (Section 5).

Additionally, our library comes with a small demo, and tutorials for getting to know the library and for formalizing your own variability languages (see "Tutorials" section below). When run in a terminal, our demo will show a translation roundtrip, showcasing the circle of compilers developed for identifying the map of variability languages (Section 5).

This section gives you a short "Getting Started" guide. For detailed instructions on setting up dependencies, see the next section. We tested our setup on Manjaro, NixOS, Windows Subsystem for Linux (WSL2), and we also tested the Docker setup on Windows 11 and macOS Ventura 13.0.1 (22A400) on an Apple M1 Pro.

In case of problems, there is a "Troubleshooting" section at the bottom of this file.

Clone the library and its submodules to a directory of your choice:

git clone --recursive https://github.com/VariantSync/Vatras.git

There are three alternative ways to compile the library and run its small demo. Either use Nix, Docker, or install Agda manually. In general, we recommend Nix because it creates a sandbox environment with all dependencies satisfied while not affecting your system setup (as does Docker), as well as giving you the opportunity to adapt and reuse the library in your own Agda projects (Docker requires to rebuild an image after every change).

• For Windows users, we recommend Docker. If you are familiar with Windows Subsystem for Linux (WSL2), you may safely use the other alternatives in WSL2, too. To install WSL2, follow the official instructions.
• For Mac users, we recommend Nix or Docker. (We experienced problems with installing Agda manually.)
• For Linux users, any alternative is fine but we recommend Nix for the reasons mentioned above.

There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose.. The only dependency of our library is the Agda standard library which is shipped as a git submodule within the agda-stdlib directory and is taken care of automatically by our makefile.

Note that building for the first time (or running nix-shell) will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min and a lot of terminal output).

The installation of Nix depends on your operating system. Head to the NixOS website and follow the installation instructions for your system. Follow the download instructions for Nix: the package manager, not NixOS: the Linux distribution! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal terminal, you can install Nix by following the instructions for installing Nix on linux from the NixOS website.

When you have Nix installed on your system, open a terminal, navigate to this directory, and then simply open a Nix shell by typing

nix-shell

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. To compile the library and run the demo, simply run make:

make

The expected output is explained in detail in the Step-by-Step guide below.

Alternatively, the demo can be compiled locally to ./result/bin.

nix-build

and then run via:

./result/bin/Vatras

How to install Docker depends on your operating system. For Windows or Mac, you can find download and installation instructions here. On Linux, installing Docker depends on your distribution. The chances are high that Docker is part of your distributions package database. Docker's documentation contains instructions for common distributions.

Once you have installed Docker, start the Docker daemon. On Windows, open the search bar using the 'Windows Key' and search for 'Docker' or 'Docker Desktop'. On Linux, the docker daemon typically runs automatically, so there is nothing to do; otherwise, start Docker's service using your service manager (e.g., with systemd, execute sudo systemctl start docker). More detailed instructions on starting the deamon are given here on the docker website.

Afterwards, open a terminal and navigate to this repository's directory (the directory containing this README.md). First, you must create the docker image:

docker build -t vatras .

Optionally, you may verify that the image was created successfully by running

docker images

and checking that an image called vatras is listed.

You can then run the demo by running the Docker image:

docker run -t vatras

The library needs Agda version 2.6.4.3 (newer version should also work but we did not test them). There are different ways to install Agda. Following the [Agda book's installation instructions], we recommend using GHCup to install GHC, Cabal, and Agda as follows (You may skip steps for tools you have already installed but there might be compatibility errors with some versions):

0. Install GHCup, which we recommend for installing ghc and cabal.

   curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh 

1. Install the GHC compiler and the cabal build tool with GHCup.

   ghcup install ghc 9.2.4
   ghcup install cabal recommended
   
   ghcup set ghc 9.2.4
   ghcup set cabal recommended

2. Install Agda (this may take a while).

   cabal update
   cabal install Agda-2.6.4.3

   To test whether the installation worked or whether your existing installation of Agda has the right version you can check the following command's output:

   > agda --version
   Agda version 2.6.4.3

In case of confusion or trouble, we recommend to check the official installation instructions, or follow the Getting-Started guide in the Programming Language Foundations in Agda book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file.

To test whether your setup is correct, and to run the demo you may use our makefile. 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. Then run

make

which will compile the library and run its small demo. The expected output is explained in detail in the Step-by-Step guide below.

The "Kick-The-Tires" section above basically explains all necessary steps to get the library up and running. Here, we give additional instructions on the expected output and how to play with other demo inputs. For using the library once you finished the setup, please have a look at the later Reusability Guide, which, among other information, includes an overview of the library, notes on our mechanized proofs, and tutorials for getting to know the 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.

export AGDA_DIR="path/to/this/repository/libs"

Beware that setting the variable will overwrite any previously set directory. In that case you might want to overwrite the variable only temporarily while working on this project.

The demo will print a long terminal output of about 1250 lines. A copy of the expected output can be found in the expected-output.txt.

First, the demo prints unicode characters to terminal, as a test for you to see whether your terminal supports unicode. The first lines should look like this.

It's dangerous to go alone! Take this unicode to see whether your terminal supports it:
  ₙ ₁ ₂ 𝕃 ℂ 𝔸 ⟦ ⟧ ⟨ ⟩ ❲❳
... but now on to the demo

The actual demo will then print:

• some translations from option calculus (OC) to binary choice calculus (2CC),
• some examples for feature structure tree composition, and
• two round-trip translations, following our circle established in the paper: CCC → ⌈e⌉-CC → 2-CC → 2CC → ADT → VariantList (CaO) → CCC. The first round-trip will translate a trivial choice D ⟨ l , r ⟩. The second round-trip will translate the sandwich expression from our paper (Expression 1). Prepare for a long terminal output because of exponential blowups for ADT and VariantList. ;)

Our library was designed to be reusable in other research endeavors or tools for studying or analyzing static variability. In particular, our library provides,

• formalizations of common variability languages as algebraic data types, including their abstract syntax and semantics (see Section 3 in our paper), and sometimes functions or proofs of their properties (e.g., for algebraic decision trees, we have implemented a dead-branch elimination and proved it correct). Previously, most of these languages were only defined on paper. These formalizations can be reused to implement variational analyses or more practice-oriented variability languages. (Our formalization might even serve as teaching material for courses on software variability in the future.)
• proven-to-be correct compilers, which translate common variability languages into each other (see Section 5 in our paper). The compilers can be reused to, for example, translate datasets or inputs to reuse analysis formulated based on a particular language to all other languages which are less or equally expressive.
• a means to conduct basic sanity checks for language designers, such as soundness or completeness. Language designers can relate new languages to existing ones with only one or two translations with respective proofs without having to compare to each language individually.
• a reusable implementation of indexed sets that can be used to talk about subsets of types in terms of functions.
• a small pretty-printing library which we use for the terminal output of our demo.
• a range of tutorials guiding you through the process of creating your own language and comparing it to existing ones, eventually concluding completeness and soundness either for free or by yourself. In the future, these tutorials might even serve as teaching material for courses on software variability.

The library is organized as follows:

• The src/Vatras/Framework directory contains the definitions of our formal framework, defined in Section 4 in our paper.
  • VariabilityLanguage.agda defines variability languages and their denotational semantics.
  • Soundness and completeness are defined in the Properties sub-directory.
  • Definitions for expressiveness and configuration equivalence are in the Relation sub-directory.
  • Theorems for proofs for free (Section 4.4) are within the Proof sub-directory, including several additional interesting theorems, which did not fit into the paper.
• src/Vatras/Lang contains definitions of particular variability languages (Section 3).
• src/Vatras/Translation/LanguageMap.lagda.md contains an overview of our case study (Section 5) to compare existing variability languages.
  • src/Vatras/Translation/Lang contains the compilers and the resulting expressiveness proofs in one file per language pair and direction (e.g., 2CC-to-ADT implements the translation from binary choice calculus to algebraic decision trees and its correctness proof).
  • Further sub-directories of src/Vatras/Translation/Lang facilitate intra-language compilers (i.e., compilers from a language to itself). For example, src/Vatras/Translation/Lang/ADT/DeadElim.agda implements a compiler from ADT to ADT that eliminates any dead branches, and additionally generates a proof that the returned ADT does not have any dead branches anymore.
• src/Vatras/Data/IndexedSet.lagda.md implements the theory of indexed sets with various operators and equational reasoning.
• src/Vatras/Test contains our unit test infrastructure (or better: unit proofs) as well as some example expressions for some languages.
• src/Vatras/Test/Experiments/RoundTrip.agda implements the round-trip for our demo, including our sandwich running example. This file may serve as an entry point and example on how to run the compilers implemented in the library.
• src/Vatras/Tutorial contains tutorials for getting to know the library (explained in more detail below).
• src/Vatras/Show/Lines.agda implements a small pretty-printer, which we use for the demo's output.

To extend or reuse the library, we offer a range of tutorials in the Tutorials module. These tutorials are literate Agda files with holes for you to fill in. Hence, when trying the tutorials you can directly check your definitions to be type-correct with Agda in a suitable editor (e.g., Emacs or VS Code) and you can navigate the framework. The tutorials might also serve as copy-and-paste-templates for new definitions.

1. The New Language Tutorial explains how to define a new variability language, including syntax, semantics, and configuration.
2. The Translation Tutorial explains how to compile/translate your language to another existing language and proving correctness.
3. The Proofs Tutorial explains how to prove completeness, soundness, and expressiveness, and how you can use your compiler to do so.

We recommend following the tutorials in order.

The code base is documented thoroughly, in terms of inline comments for most definitions. For some of the crucial files or proof steps, we use literate Agda (mostly Markdown) to explain proofs step-by-step. In terms of tutorials (see above), we provide a detailed introduction to the library and its central definitions. We refrained from providing documentation in terms of a separate website because commonly, Agda is best navigated, explored, and read from within a suitable editor (typically Emacs, Vim, or VS Code).

To adapt the demo, you can implement your own experiments and add them to the list of experiments to run at the top of the Main file. If you simply want to change the inputs of existing experiments, you can change the list of inputs for each experiment in the list of experiments as well. In particular, you may add new inputs to the round-trip translation by adding your own example core choice calculus expression (CCC) to the examples list at the bottom of the RoundTrip module. You may define your own expression by adding a new definition like this, where ex-new is the name of your example, "The new example" is its title, and where {!!} is an Agda hole which you can fill in with an abstract syntax tree of a core choice calculus expression:

ex-new : Example (CCC.CCC Feature ∞ Artifact)
ex-new = "The new example" ≔ {!!}

Then add your new list to the examples list at the bottom of the file.

When using Nix, you can use this repository as a library in you own project, by using agda.withPackages:

agda = nixpkgs.agda.withPackages [
  nixpkgs.agdaPackages.standard-library
  (import /path/to/this/git/repository {
    pkgs = nixpkgs;
  })
];

Though, not required, we recommend to use the nixpkgs pin created using niv provided in this repository to minimize version conflicts.

After downloading this library, you can register it by appending the path of Vatras.agda-lib to the file $AGDA_DIR/libraries, creating it if necessary. If the environment variable AGDA_DIR is unset, it defaults to ~/.agda on unix-like systems and C:\Users\USERNAME\AppData\Roaming\agda or similar on Windows. After registering this library on your system, you can use it in your project by stating Vatras as a dependency in your Agda library file. An Agda library file has the suffix .agda-lib and is usually contained in the root directory of your project. Its content, including the dependency to Vatras, should include the following:

name: YOUR-PROJECT-NAME
depend: Vatras
include: SOME/PATH/IN/YOUR/PROJECT

For details about Agda's library management, please have a look at Agda's packaging guide.

Our Agda formalization exhaustively formalizes all definitions, theorems, and proofs from our paper. The following table shows where each of the definitions, theorems, and proofs from the paper are formalized in this library.

Some formalizations in the library differ slightly from their in-paper-representation:

• A few definitions and proofs in this library generalize over the type of variants V : 𝕍. In the paper, this type is fixed to rose trees (see Definition 3.1, trees where each node can have any number of children), which we also formalized in src/Vatras/Framework/Variants.agda as type Rose. This generalization allows us to also formalize variability languages that (1) have other variant types such as Gruler's language (see src/Vatras/Lang/Gruler.agda, Section 3.6 in the paper), or (2) are independent of the variant type, such as clone and own (Section 5.2 in the paper).
• Also generalizing over the annotation language F : 𝔽 was rather easy in the paper (Section 3.3) but requires to carry around that 𝔽 explicitly in Agda in definitions and theorems a lot.

Except for the Agda standard-library, this library has no dependencies, as explained in the setup instructions above. In particular, this means we do not rely on other proof frameworks.

Our library consists of many proofs. Their organization into multiple files is presented in the Overview section, and the Paper-to-Library table above. Proofs are documented inline via comments in the code (also see the Documentation section above).

Our library, does not use any of the following assumptions or axioms in central parts of the code:

1. no additional axioms via postulate (e.g., no extensionality or excluded middle)
2. no termination macros ({-# TERMINATING -#}). All functions and proofs are proven to terminate (for proofs this means they use well-founded induction or are non-cyclic).
3. no unfinished proofs (i.e., there are no holes {! !}).

Of course, there are three exceptions to this.

For the tutorials (see above), we deliberately use many holes. These holes are intended to be exercises for someone who is working through the tutorial. We also use a terminating macro here to avoid sized types to keep the tutorial simple. The place where we use the macro is proven to terminate throughout the rest of the library multiple times, by using sized types.

For termination checking, we use sized types, which currently have known inconsistencies. The risks of using them in inconsistent ways are often accepted because they can simplify proofs substantially. We came to the same conclusion and tried our best to use them without interaction with more complicated language features to reduce the likelihood of encountering an inconsistency. In particular, we use sized types only in a very basic, inductive way and:

• We do not use coinductive data types (#7178, #1946, #1201).
• We do not use Size< (#6002).
• We do not compare Size for equality (#2820).

For a non-crucial part of our framework, we included four postulates, which assume that two primitive operations from the standard library are invertible:

• converting Strings to lists of characters and vice versa,
• converting characters to natural numbers and vice versa.

These postulates can be found in src/Vatras/Util/String.agda. We believe these postulates to be reasonable because strings are commonly defined as lists of characters, and because characters are usually encoded as natural numbers in text encodings (e.g., UTF-8). We use these axioms as an example, to prove that we can simplify annotations String × ℕ to just String, by turning a pair s , n into a String representation s "." show n. This simplification only exists to beautify theorems (so they do not have to mention the pair) and align them more closely to our paper but our results would remain the same without that simplification. In fact, some of these postulates are an open issue #6119 in the Agda implementation.

• The library currently only supports abstract syntax for all languages. There are no parsers, so it is not yet possible to read in files or strings of concrete syntax. This is not a claim of the paper though and would just be a nice additional feature.

If you see an error similar to this one

.../src/MAlonzo/Code/Vatras/Data/IndexedSet.hs:1705:3: error:
    Not in scope:
      type constructor or class ‘MAlonzo.Code.Agda.Primitive.T_Level_14’
    Perhaps you meant ‘MAlonzo.Code.Agda.Primitive.T_Level_18’ (imported from MAlonzo.Code.Agda.Primitive)
    Module ‘MAlonzo.Code.Agda.Primitive’ does not export ‘T_Level_14’.
     |
1705 |   MAlonzo.Code.Agda.Primitive.T_Level_14 ->
     |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

there might be corrupt build files. Simply run make clean.

If you see an error similar to this one

It's dangerous to go alone! Take this unicode to see whether your terminal supports it:
   Vatras: <stdout>: commitAndReleaseBuffer: invalid argument (cannot encode character '\8345')

there might be a problem with your terminal settings. In particular, this error is caused by the Haskell runtime failing to detect UTF-8 support of your terminal. This might be caused by your terminal not actually supporting Unicode, or, more likely, misdetection of the Unicode capabilities of your terminal. Simply set the environment variable LC_ALL to C.UTF-8 by, for example, running export LC_ALL=C.UTF-8 before running Vatras, to force Unicode detection.

The first lines the demo prints should be

It's dangerous to go alone! Take this unicode to see whether your terminal supports it:
  ₙ ₁ ₂ 𝕃 ℂ 𝔸 ⟦ ⟧ ⟨ ⟩ ❲❳
... but now on to the demo.

The second line should not be empty, nor should it contain Unicode replacement characters or characters with accents. Instead, it should contain mathematical symbols. There are two possible causes if you do not see the mathematical symbols:

• The font you are using is missing the required symbols. In this case you can use a different font as a fallback or switch to a different font altogether. A common font supporting all required symbols is Symbola.

• Your terminal does not support UTF-8 correctly. In this case you have to switch to a different terminal.

If you see an error like

 failed due to signal 9 (Killed)
------
Dockerfile:19
--------------------
  17 |
  18 |     # Verify all proofs and build the demo.
  19 | >>> RUN nix-build
  20 |
  21 |     # Copy the demo with all runtime dependencies (ignoring build-time dependencies)
--------------------
ERROR: failed to solve: process "/bin/sh -c nix-build" did not complete successfully: exit code: 100

during a Docker build, you might have encountered an out of memory issue. Try to rerun the same command after closing other applications which might comsume a lot of RAM. In some cases it may also be necessary to disable some kind of out-of-memory killer (also known as OOM killer or OOM deamon) but use this option with caution.

The following error may occur when executing make after a manual setup:

Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib.
Reason: ./libs/../agda-stdlib/standard-library.agda-lib: openBinaryFile: does not exist (No such file or directory)
make: *** [makefile:15: build] Error 42

This error indicates that the agda-stdlib git submodule has not been set up correctly. Executing git submodule update --init in the root of the repository should fix the problem.

The name Vatras is (of course) an acronym, which stands for VAriability language TRAnslationS. Besides, Vatras is a water mage in the classic german RPG Gothic II, who is praying to the god Adanos, who brings "some kind of equality" very loosely speaking.