The following sequence of commands succeeds if Agda 2.6.3 is used (if --trace-imports=0 is replaced by -vimport:0), but fails with a recent development version:
$ mkdir fresh && cd fresh > /dev/null
$ (git clone https://github.com/agda/agda-stdlib.git && cd agda-stdlib && git checkout v1.7.2) >& /dev/null
$ (git clone https://github.com/fhlkfy/logrel-mltt && cd logrel-mltt && git checkout d528b80aebec2268a11818cf125253e9ea83f672) >& /dev/null
$ printf '\nname: logrel-mltt' >> logrel-mltt/logrel-mltt.agda-lib
$ cat > libraries <<EOF
$PWD/agda-stdlib/standard-library.agda-lib
$PWD/logrel-mltt/logrel-mltt.agda-lib
EOF
$ agda --no-default-libraries --library-file=libraries -lstandard-library -llogrel-mltt --trace-imports=0 logrel-mltt/Definition/LogicalRelation/Substitution/Introductions/Natrec.agda
Failed to solve the following constraints:
[…]
Unsolved metas at the following locations:
[…]
Bisection points to "[ fix #5837 ] Make occurs checker type-directed" (5467b25). @jespercockx, can you take a look at this?
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