Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/7044 below:

Serializer crashes on blocked definitions when using --allow-unsolved-metas · Issue #7044 · agda/agda · GitHub

During tinkering with agda-unimath repo (and in the process, resetting all definitions to holes), I've encountered an "IMPOSSIBLE" bug.

I reduced the error to a few files: impossible.zip

From the src directory, after extracting the attached zip file, invoke agda .\foundation\action-on-identifications-functions.lagda.md --allow-unsolved-metas.

Agda checks the files successfully.

An internal error has occurred. Please report this as a bug.
Location of the error: IMPOSSIBLE, called at src/full\Agda\TypeChecking\Serialise\Instances\Internal.hs:232:21 in Agda-2.6.2.2-I0mdgVgXQQ9I75Kwxokerz:Agda.TypeChecking.Serialise.Instances.Internal

I am able to reproduce this both in native Windows and WSL, so it seems independent of the OS.

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