Propriétaire

agda

Se connecter pour suivre

5 dépôts indexés · Voir sur GitHub

Accessible aux débutants Tout
Ouverte Toutes

Les issues sur lesquelles quelqu’un travaille peut-être déjà sont listées en dernier. Tout trier par date

  • Builtin imports fail with "COMPILE pragma not allowed in safe mode" when the data directory's `lib` or `lib/prim` is a symlink
    Ouverte
    • Quelque chose ne va pas ?

    Difficulté 2/5 1-3 heures Accessibilité débutants 72/100

    agda/agda#8897 ·

    Les mainteneurs répondent en général sous 1 jour

  • Skipping compilation for up-to-date files results in mis-compilation
    Ouverte
    • Quelque chose ne va pas ?
    bug

    Difficulté 3/5 1-2 jours Accessibilité débutants 52/100

    agda/agda2hs#486 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • `opaque unfolding` and `REWRITE` rules breaks subject reduction
    Ouverte
    • Quelque chose ne va pas ?
    confluence opaque subject reduction

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 35/100

    agda/agda#8893 · 4 commentaires · 3 réactions ·

    Les mainteneurs répondent en général sous 1 jour

  • Warning that has been turned off is reported
    Ouverte
    • Quelque chose ne va pas ?
    PR welcome type: bug ux: warnings

    Difficulté 4/5 1-2 jours Accessibilité débutants 55/100

    agda/agda#8886 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • 2.8.0: slow "undefined" report
    Ouverte
    • Quelque chose ne va pas ?
    status: MWE needed

    Difficulté 4/5 3-5 jours Accessibilité débutants 25/100

    agda/agda#8885 · 3 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Compare things with α-equivalence
    Ouverte
    • Quelque chose ne va pas ?
    bug

    Difficulté 3/5 1-2 jours Accessibilité débutants 57/100

    agda/agda2hs#479 ·

    Les mainteneurs répondent en général sous 1 jour

  • Bulk hidden arguments
    Ouverte
    • Quelque chose ne va pas ?
    hidden arguments type: enhancement

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 24/100

    agda/agda#8872 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Support type operators in rewrite rules
    Ouverte
    • Quelque chose ne va pas ?
    enhancement

    Difficulté 4/5 1-2 jours Accessibilité débutants 45/100

    agda/agda2hs#473 ·

    Les mainteneurs répondent en général sous 1 jour

  • `COMPILE to` definitions from `Haskell.*` modules
    Ouverte
    • Quelque chose ne va pas ?
    enhancement

    Difficulté 4/5 3-5 jours Accessibilité débutants 48/100

    agda/agda2hs#472 · 1 réaction ·

    Les mainteneurs répondent en général sous 1 jour

  • Compile abstract datatype/record
    Ouverte
    • Quelque chose ne va pas ?
    enhancement

    Difficulté 4/5 3-5 jours Accessibilité débutants 48/100

    agda/agda2hs#471 · 1 réaction ·

    Les mainteneurs répondent en général sous 1 jour

  • `haskell-src-exts` currently on life support
    Ouverte
    • Quelque chose ne va pas ?

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 25/100

    agda/agda2hs#468 ·

    Les mainteneurs répondent en général sous 1 jour

  • Opaque control from reflection API
    Ouverte
    • Quelque chose ne va pas ?
    opaque reflection type: enhancement

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 35/100

    agda/agda#8861 · 1 réaction ·

    Les mainteneurs répondent en général sous 1 jour

  • Control over reduction during elaboration
    Ouverte
    • Quelque chose ne va pas ?
    performance type: discussion type: enhancement

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 25/100

    agda/agda#8860 · 4 commentaires · 6 réactions ·

    Les mainteneurs répondent en général sous 1 jour

  • macOS deploy broken (macos-26-arm64, image version 20261013.0424.1)
    Ouverte
    • Quelque chose ne va pas ?
    infra: github workflows upstream

    Difficulté 3/5 1-2 jours Accessibilité débutants 20/100

    agda/agda#8845 · 5 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Macro defined in a module does not respect parameter binding
    Ouverte
    • Quelque chose ne va pas ?
    parameters reflection

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 15/100

    agda/agda#8844 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • When injectivity (constructor-headedness) leads to a hard error, can Agda communicate this?
    Ouverte
    • Quelque chose ne va pas ?
    injectivity type: enhancement ux: error reporting

    Difficulté 4/5 3-5 jours Accessibilité débutants 30/100

    agda/agda#8814 ·

    Les mainteneurs répondent en général sous 1 jour

  • Improve "refine" interactive command: currently fails with more than 10 arguments
    Ouverte
    • Quelque chose ne va pas ?
    type: enhancement ux: interaction

    Difficulté 4/5 3-5 jours Accessibilité débutants 32/100

    agda/agda#8813 ·

    Les mainteneurs répondent en général sous 1 jour

  • Better error reporting for failed meta instantiations
    Peut-être à nouveau libre Ouverte
    • Quelque chose ne va pas ?
    meta ux: error reporting

    agda/agda#8796 · 1 réaction · 1 personne assignée ·

    Les mainteneurs répondent en général sous 1 jour

  • `ClashesViaRenaming` too strict
    Ouverte
    • Quelque chose ne va pas ?
    difficulty: easy import ux: warnings

    Difficulté 4/5 3-5 jours Accessibilité débutants 35/100

    agda/agda#8786 ·

    Les mainteneurs répondent en général sous 1 jour

  • Positivity checker loses information through module applications
    Peut-être à nouveau libre Ouverte
    • Quelque chose ne va pas ?
    polarity positivity type: enhancement

    agda/agda#8773 · 1 commentaire · 1 personne assignée ·

    Les mainteneurs répondent en général sous 1 jour

  • The strict GHC backend generates code that segfaults
    Ouverte
    • Quelque chose ne va pas ?
    backend: ghc ghc issue upstream

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 8/100

    agda/agda#8764 · 6 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Compare agda2hs to the GHC backend
    Ouverte
    • Quelque chose ne va pas ?
    backend: ghc performance

    Difficulté 4/5 3-5 jours Accessibilité débutants 25/100

    agda/agda#8761 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Documentation: group pages in "Language Reference" by topic
    Ouverte
    • Quelque chose ne va pas ?
    type: enhancement ux: documentation

    Difficulté 3/5 Une demi-journée Accessibilité débutants 35/100

    agda/agda#8760 · 1 commentaire · 4 réactions ·

    Les mainteneurs répondent en général sous 1 jour

  • Erasure-aware pattern matching
    Ouverte
    • Quelque chose ne va pas ?
    erasure language change pattern matching

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 6/100

    agda/agda#8758 ·

    Les mainteneurs répondent en général sous 1 jour

  • Quality-of-life improvements to opaque
    Ouverte
    • Quelque chose ne va pas ?
    opaque type: enhancement

    Difficulté 4/5 3-5 jours Accessibilité débutants 30/100

    agda/agda#8757 · 3 réactions ·

    Les mainteneurs répondent en général sous 1 jour

  • Strange bug w/ indexed HITs in --cubical
    Ouverte
    • Quelque chose ne va pas ?

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 8/100

    agda/agda#8753 · 3 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Associativity declarations for pre and post fix operators
    Ouverte
    • Quelque chose ne va pas ?
    operators type: discussion

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 15/100

    agda/agda#8750 · 6 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Should we allow λ with empty `where` block as absurd lambda?
    Ouverte
    • Quelque chose ne va pas ?
    absurd clauses parser type: enhancement

    Difficulté 4/5 3-5 jours Accessibilité débutants 22/100

    agda/agda#8747 · 8 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Shiki highlighting: contribute Agda grammar
    Ouverte
    • Quelque chose ne va pas ?
    type: enhancement ux: highlighting

    Difficulté 3/5 1-2 jours Accessibilité débutants 35/100

    agda/agda#8742 ·

    Les mainteneurs répondent en général sous 1 jour

  • JS backend does not check type of `main`
    Ouverte
    • Quelque chose ne va pas ?
    backend: js

    Difficulté 3/5 1-2 jours Accessibilité débutants 45/100

    agda/agda#8741 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Refuse to compile unsupported `LitMeta` to JS
    Ouverte
    • Quelque chose ne va pas ?
    backend: js reflection

    Difficulté 2/5 1-3 heures Accessibilité débutants 56/100

    agda/agda#8735 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • JS backend still removes some function parameters
    Ouverte
    • Quelque chose ne va pas ?
    backend: js erasure projection-like

    Difficulté 4/5 3-5 jours Accessibilité débutants 25/100

    agda/agda#8734 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Cannot give in types of `variable`s
    Peut-être à nouveau libre Ouverte
    • Quelque chose ne va pas ?
    generalize ux: interaction

    agda/agda#8728 · 1 personne assignée ·

    Les mainteneurs répondent en général sous 1 jour

  • Broken precondition in the termination checker
    Ouverte
    • Quelque chose ne va pas ?
    debug status: MWE needed termination

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 22/100

    agda/agda#8721 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • [Moderate fix] The internal type checker does not check the boundary conditions of cubical terms
    Ouverte
    • Quelque chose ne va pas ?
    cubical false with

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 8/100

    agda/agda#8689 · 4 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Option `-WerrorWarningName`
    Ouverte
    • Quelque chose ne va pas ?
    ux: options ux: warnings

    Difficulté 4/5 3-5 jours Accessibilité débutants 30/100

    agda/agda#8684 · 4 commentaires · 2 réactions ·

    Les mainteneurs répondent en général sous 1 jour

  • GS-Monoidal categories
    Ouverte
    • Quelque chose ne va pas ?

    Difficulté 4/5 3-5 jours Accessibilité débutants 22/100

    agda/agda-categories#547 · 1 commentaire ·

  • Snippet causing Agda to loop
    Ouverte
    • Quelque chose ne va pas ?
    Agda loops workaround exists

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 12/100

    agda/agda#8641 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Remove odd syntax from Categories.Category.Construction.Core
    Peut-être à nouveau libre Ouverte
    • Quelque chose ne va pas ?

    agda/agda-categories#536 · 1 personne assignée ·

  • findFile'': nubOn id does not resolve symlinks, causing false AmbiguousTopLevelModuleName
    Ouverte
    • Quelque chose ne va pas ?
    file system

    Difficulté 3/5 1-2 jours Accessibilité débutants 64/100

    agda/agda#8608 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • When .agda and .agdai are updated on disk, highlighting is from the future
    Ouverte
    • Quelque chose ne va pas ?
    ux: emacs ux: highlighting

    Difficulté 4/5 3-5 jours Accessibilité débutants 30/100

    agda/agda#8597 ·

    Les mainteneurs répondent en général sous 1 jour

  • A strange message about "unsolved" thing
    Ouverte
    • Quelque chose ne va pas ?
    meta type: enhancement ux: error reporting

    Difficulté 4/5 3-5 jours Accessibilité débutants 30/100

    agda/agda#8595 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Make a release to match stdlib v2.4
    Peut-être à nouveau libre Ouverte
    • Quelque chose ne va pas ?

    agda/agda-categories#529 · 1 personne assignée ·

  • Typechecking certain parametrized modules is much slower than expected
    Ouverte
    • Quelque chose ne va pas ?
    modules parameters performance

    Difficulté 4/5 3-5 jours Accessibilité débutants 20/100

    agda/agda#8589 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Instance-search instances get inlined
    Ouverte
    • Quelque chose ne va pas ?
    enhancement

    Difficulté 4/5 3-5 jours Accessibilité débutants 45/100

    agda/agda2hs#458 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • OOM with deep-matching / with(?)
    Ouverte
    • Quelque chose ne va pas ?
    performance status: duplicate with

    Difficulté 4/5 3-5 jours Accessibilité débutants 20/100

    agda/agda#8582 · 2 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • agda2hs cannot compile Traversable instances defined with `traverse=_`
    Ouverte
    • Quelque chose ne va pas ?
    bug library

    Difficulté 4/5 1-2 jours Accessibilité débutants 50/100

    agda/agda2hs#457 · 1 commentaire ·

    Les mainteneurs répondent en général sous 1 jour

  • Inconsistency with univalence because of termination checker
    Ouverte
    • Quelque chose ne va pas ?
    cubical false termination type: bug univalence

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 5/100

    agda/agda#8572 ·

    Les mainteneurs répondent en général sous 1 jour

  • Proposal: allow `with` to give up
    Ouverte
    • Quelque chose ne va pas ?
    performance type: discussion with

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 18/100

    agda/agda#8571 · 4 commentaires ·

    Les mainteneurs répondent en général sous 1 jour

  • Incorrect handling of simplicial sets and Kan complexes.
    Ouverte
    • Quelque chose ne va pas ?

    Difficulté 5/5 Plus d'une semaine Accessibilité débutants 25/100

    agda/agda-categories#526 · 1 commentaire ·

Affichage des 100 plus récents

Cette page ne liste que les entrées les plus récentes. Le filtre avancé contient l'inventaire complet, affiné par langage, difficulté et durée.

Ouvrir le filtre avancé

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.