Agda accepts several .agda-lib files for a project in the same project root and then takes their union (of dependencies, include directories, flags). However, for flags that contradict each other this "union" is order-dependent. The order is presumably determined by how the host OS lists the .agda-lib files. Thus, the order may vary between OSs, and also, if the order is dependent on file creation order, than even on a single OS, the result could be non-deterministic.
Here is a script to create such situations:
#!/bin/sh
DIR=yes-no
mkdir -p ${DIR}
cat > ${DIR}/Main.agda <<EOF
data Empty : Set where
f : Empty
f = f
EOF
cat > ${DIR}/ja.agda-lib <<EOF
include: .
flags: --termination-check
EOF
cat > ${DIR}/nej.agda-lib <<EOF
include: .
flags: --no-termination-check
EOF
agda-2.8.0 -i${DIR} ${DIR}/Main.agda
## ACCEPTED
DIR=no-yes
mkdir -p ${DIR}
cat > ${DIR}/Main.agda <<EOF
data Empty : Set where
f : Empty
f = f
EOF
cat > ${DIR}/no.agda-lib <<EOF
include: .
flags: --no-termination-check
EOF
cat > ${DIR}/yes.agda-lib <<EOF
include: .
flags: --termination-check
EOF
agda-2.8.0 -i${DIR} ${DIR}/Main.agda
## REJECTED with termination error
Why do we allow several .agda-lib files in the first place? What is the use case for that?
And if there is a use case, shouldn't we check that these files do not make contradictory choices on flags?
ATTN: @UlfNorell @nad @jespercockx @plt-amy
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4