Skip to content

Conversation

pmbittner and others added 25 commits August 8, 2025 09:33
This compiler is an adapted version of the VariantList-to-VT compiler.
It turned out to be simpler and a better separation of concerns to split
the VariantList-to-VT compiler into two compilers:
VariantList-to-ADT (introduced in this commit) and an ADT-to-VT
compiler (introduced in a previous commit).
Hence, the VariantList-to-ADT compiler and its proofs are a simplified
copy of the VariantList-to-VT compiler.
This makes the proofs also visible when importing the module with a
consistent naming scheme. We write "...-on" when the variant type is a parameter.
Union, Intersection, Set Difference and Further Operations on Indexed Sets
After a cache hit, there are no channels installed. When running
`nix-shell`, it tries to execute bash from a nixpkgs in a channel, fails
to do so and falls back to the bash in the environment. Unfortunately,
the warning message is quite misleading:
```
warning: Nix search path entry 'channel:' cannot be downloaded, ignoring
error:
       … while calling the 'import' builtin

         at «string»:1:2:

            1| (import <nixpkgs> {}).bashInteractive
             |  ^

       … while realising the context of a path

       … while calling the 'findFile' builtin

         at «string»:1:9:

            1| (import <nixpkgs> {}).bashInteractive
             |         ^

       error: file 'nixpkgs' was not found in the Nix search path (add it using $NIX_PATH or -I)
will use bash from your environment
```
As there is no further output it looks like a failed CI run although the exit code was zero and thus the CI is considered successful (which is indeed correct).

This fix explicitly uses the environment if no channels are installed.
Note that channels are still used if available. In particular, the shell
used when the cache hits is the pre-installed one but on cache misses
the shell is taken from nixpkgs. Both shells are bash but the versions
might differ.
Simplified Variation Tree Completeness Proof
@ibbem ibbem merged commit 5765694 into main Oct 14, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants