Owner

agda

Zum Folgen anmelden

5 indexierte Repositories · Auf GitHub ansehen

Einsteigerfreundlich Alles
Offen Alle

Issues, an denen vielleicht schon jemand arbeitet, stehen am Ende. Alles nach Datum anzeigen

  • Builtin imports fail with "COMPILE pragma not allowed in safe mode" when the data directory's `lib` or `lib/prim` is a symlink
    Offen
    • Stimmt etwas nicht?

    Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 72/100

    agda/agda#8897 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Skipping compilation for up-to-date files results in mis-compilation
    Offen
    • Stimmt etwas nicht?
    bug

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 52/100

    agda/agda2hs#486 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • `opaque unfolding` and `REWRITE` rules breaks subject reduction
    Offen
    • Stimmt etwas nicht?
    confluence opaque subject reduction

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 35/100

    agda/agda#8893 · 4 Kommentare · 3 Reaktionen ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Warning that has been turned off is reported
    Offen
    • Stimmt etwas nicht?
    PR welcome type: bug ux: warnings

    Schwierigkeit 4/5 1-2 Tage Anfängerfreundlichkeit 55/100

    agda/agda#8886 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • 2.8.0: slow "undefined" report
    Offen
    • Stimmt etwas nicht?
    status: MWE needed

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 25/100

    agda/agda#8885 · 3 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Compare things with α-equivalence
    Offen
    • Stimmt etwas nicht?
    bug

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 57/100

    agda/agda2hs#479 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Bulk hidden arguments
    Offen
    • Stimmt etwas nicht?
    hidden arguments type: enhancement

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 24/100

    agda/agda#8872 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Support type operators in rewrite rules
    Offen
    • Stimmt etwas nicht?
    enhancement

    Schwierigkeit 4/5 1-2 Tage Anfängerfreundlichkeit 45/100

    agda/agda2hs#473 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • `COMPILE to` definitions from `Haskell.*` modules
    Offen
    • Stimmt etwas nicht?
    enhancement

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 48/100

    agda/agda2hs#472 · 1 Reaktion ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Compile abstract datatype/record
    Offen
    • Stimmt etwas nicht?
    enhancement

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 48/100

    agda/agda2hs#471 · 1 Reaktion ·

    Maintainer antworten meist innerhalb von 1 Tag

  • `haskell-src-exts` currently on life support
    Offen
    • Stimmt etwas nicht?

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 25/100

    agda/agda2hs#468 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Opaque control from reflection API
    Offen
    • Stimmt etwas nicht?
    opaque reflection type: enhancement

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 35/100

    agda/agda#8861 · 1 Reaktion ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Control over reduction during elaboration
    Offen
    • Stimmt etwas nicht?
    performance type: discussion type: enhancement

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 25/100

    agda/agda#8860 · 4 Kommentare · 6 Reaktionen ·

    Maintainer antworten meist innerhalb von 1 Tag

  • macOS deploy broken (macos-26-arm64, image version 20261013.0424.1)
    Offen
    • Stimmt etwas nicht?
    infra: github workflows upstream

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 20/100

    agda/agda#8845 · 5 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Macro defined in a module does not respect parameter binding
    Offen
    • Stimmt etwas nicht?
    parameters reflection

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 15/100

    agda/agda#8844 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?
    Offen
    • Stimmt etwas nicht?
    injectivity type: enhancement ux: error reporting

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 30/100

    agda/agda#8814 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Improve "refine" interactive command: currently fails with more than 10 arguments
    Offen
    • Stimmt etwas nicht?
    type: enhancement ux: interaction

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 32/100

    agda/agda#8813 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Better error reporting for failed meta instantiations
    Evtl. wieder frei Offen
    • Stimmt etwas nicht?
    meta ux: error reporting

    agda/agda#8796 · 1 Reaktion · 1 zugewiesene Person ·

    Maintainer antworten meist innerhalb von 1 Tag

  • `ClashesViaRenaming` too strict
    Offen
    • Stimmt etwas nicht?
    difficulty: easy import ux: warnings

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 35/100

    agda/agda#8786 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Positivity checker loses information through module applications
    Evtl. wieder frei Offen
    • Stimmt etwas nicht?
    polarity positivity type: enhancement

    agda/agda#8773 · 1 Kommentar · 1 zugewiesene Person ·

    Maintainer antworten meist innerhalb von 1 Tag

  • The strict GHC backend generates code that segfaults
    Offen
    • Stimmt etwas nicht?
    backend: ghc ghc issue upstream

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 8/100

    agda/agda#8764 · 6 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Compare agda2hs to the GHC backend
    Offen
    • Stimmt etwas nicht?
    backend: ghc performance

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 25/100

    agda/agda#8761 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Documentation: group pages in "Language Reference" by topic
    Offen
    • Stimmt etwas nicht?
    type: enhancement ux: documentation

    Schwierigkeit 3/5 Ein halber Tag Anfängerfreundlichkeit 35/100

    agda/agda#8760 · 1 Kommentar · 4 Reaktionen ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Erasure-aware pattern matching
    Offen
    • Stimmt etwas nicht?
    erasure language change pattern matching

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 6/100

    agda/agda#8758 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Quality-of-life improvements to opaque
    Offen
    • Stimmt etwas nicht?
    opaque type: enhancement

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 30/100

    agda/agda#8757 · 3 Reaktionen ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Strange bug w/ indexed HITs in --cubical
    Offen
    • Stimmt etwas nicht?

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 8/100

    agda/agda#8753 · 3 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Associativity declarations for pre and post fix operators
    Offen
    • Stimmt etwas nicht?
    operators type: discussion

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 15/100

    agda/agda#8750 · 6 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Should we allow λ with empty `where` block as absurd lambda?
    Offen
    • Stimmt etwas nicht?
    absurd clauses parser type: enhancement

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 22/100

    agda/agda#8747 · 8 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Shiki highlighting: contribute Agda grammar
    Offen
    • Stimmt etwas nicht?
    type: enhancement ux: highlighting

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 35/100

    agda/agda#8742 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • JS backend does not check type of `main`
    Offen
    • Stimmt etwas nicht?
    backend: js

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 45/100

    agda/agda#8741 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Refuse to compile unsupported `LitMeta` to JS
    Offen
    • Stimmt etwas nicht?
    backend: js reflection

    Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 56/100

    agda/agda#8735 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • JS backend still removes some function parameters
    Offen
    • Stimmt etwas nicht?
    backend: js erasure projection-like

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 25/100

    agda/agda#8734 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Cannot give in types of `variable`s
    Evtl. wieder frei Offen
    • Stimmt etwas nicht?
    generalize ux: interaction

    agda/agda#8728 · 1 zugewiesene Person ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Broken precondition in the termination checker
    Offen
    • Stimmt etwas nicht?
    debug status: MWE needed termination

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 22/100

    agda/agda#8721 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • [Moderate fix] The internal type checker does not check the boundary conditions of cubical terms
    Offen
    • Stimmt etwas nicht?
    cubical false with

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 8/100

    agda/agda#8689 · 4 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Option `-WerrorWarningName`
    Offen
    • Stimmt etwas nicht?
    ux: options ux: warnings

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 30/100

    agda/agda#8684 · 4 Kommentare · 2 Reaktionen ·

    Maintainer antworten meist innerhalb von 1 Tag

  • GS-Monoidal categories
    Offen
    • Stimmt etwas nicht?

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 22/100

    agda/agda-categories#547 · 1 Kommentar ·

  • Snippet causing Agda to loop
    Offen
    • Stimmt etwas nicht?
    Agda loops workaround exists

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 12/100

    agda/agda#8641 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Remove odd syntax from Categories.Category.Construction.Core
    Evtl. wieder frei Offen
    • Stimmt etwas nicht?

    agda/agda-categories#536 · 1 zugewiesene Person ·

  • findFile'': nubOn id does not resolve symlinks, causing false AmbiguousTopLevelModuleName
    Offen
    • Stimmt etwas nicht?
    file system

    Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 64/100

    agda/agda#8608 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • When .agda and .agdai are updated on disk, highlighting is from the future
    Offen
    • Stimmt etwas nicht?
    ux: emacs ux: highlighting

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 30/100

    agda/agda#8597 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • A strange message about "unsolved" thing
    Offen
    • Stimmt etwas nicht?
    meta type: enhancement ux: error reporting

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 30/100

    agda/agda#8595 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Make a release to match stdlib v2.4
    Evtl. wieder frei Offen
    • Stimmt etwas nicht?

    agda/agda-categories#529 · 1 zugewiesene Person ·

  • Typechecking certain parametrized modules is much slower than expected
    Offen
    • Stimmt etwas nicht?
    modules parameters performance

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 20/100

    agda/agda#8589 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Instance-search instances get inlined
    Offen
    • Stimmt etwas nicht?
    enhancement

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 45/100

    agda/agda2hs#458 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • OOM with deep-matching / with(?)
    Offen
    • Stimmt etwas nicht?
    performance status: duplicate with

    Schwierigkeit 4/5 3-5 Tage Anfängerfreundlichkeit 20/100

    agda/agda#8582 · 2 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • agda2hs cannot compile Traversable instances defined with `traverse=_`
    Offen
    • Stimmt etwas nicht?
    bug library

    Schwierigkeit 4/5 1-2 Tage Anfängerfreundlichkeit 50/100

    agda/agda2hs#457 · 1 Kommentar ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Inconsistency with univalence because of termination checker
    Offen
    • Stimmt etwas nicht?
    cubical false termination type: bug univalence

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 5/100

    agda/agda#8572 ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Proposal: allow `with` to give up
    Offen
    • Stimmt etwas nicht?
    performance type: discussion with

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 18/100

    agda/agda#8571 · 4 Kommentare ·

    Maintainer antworten meist innerhalb von 1 Tag

  • Incorrect handling of simplicial sets and Kan complexes.
    Offen
    • Stimmt etwas nicht?

    Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 25/100

    agda/agda-categories#526 · 1 Kommentar ·

Die neuesten 100 werden angezeigt

Diese Seite listet nur das zuletzt Erfasste. Der vollständige Bestand steht im erweiterten Filter, eingegrenzt nach Sprache, Schwierigkeit und Aufwand.

Erweiterten Filter öffnen

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.