Labels

• .NET

  .NET

  Pull requests that update .NET code

• area: build-system

  area: build-system

  Support for dependencies in Dafny, generation of target language build files

• area: caching

  area: caching

  Support for caching parts of Dafny's verification pipeline

• area: error-reporting

  area: error-reporting

  Clarity of the error reporting

• area: ffi

  area: ffi

  The {:extern} attribute and otherwise interfacing with code in other languages

• area: new users

  area: new users

  Getting new users started

• area: nonlinear arithmetic

  area: nonlinear arithmetic

  Support for reasoning about nonlinear arithmetic

• area: performance

  area: performance

  Performance issues

• area: refinement

  area: refinement

  Dafny's module-refinement machinery

• autocut

  autocut

  For issues that are created by CI automation

• breaking-change

  breaking-change

  Any change that will cause existing Dafny codebases to break (excluding verification instability)

• crash

  crash

  Dafny crashes on this input, or generates malformed code that can not be executed

• dependencies

  dependencies

  Pull requests that update a dependency file

• difficulty: easy

  difficulty: easy

  Issues that should take a few days at most to fix

• difficulty: good-first-issue

  difficulty: good-first-issue

  Good first issues

• difficulty: hard

  difficulty: hard

  Issues that will take more than a week to fix

• difficulty: medium

  difficulty: medium

  Issues that should take a few days to a week to fix

• during 1: program development

  during 1: program development

  Bad error message or documentation; IDE bug; crash compiling invalid program

• during 2: compilation of correct program

  during 2: compilation of correct program

  Dafny rejects a valid program during compilation

• during 3: execution of incorrect program

  during 3: execution of incorrect program

  An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec

• during 4: bad execution of correct program

  during 4: bad execution of correct program

  A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly

• github_actions

  github_actions

  Pull requests that update GitHub Actions code

• has-workaround: no

  has-workaround: no

  There are no known workarounds

• has-workaround: yes

  has-workaround: yes

  There is a known workaround

• incompleteness

  incompleteness

  Things that Dafny should be able to prove, but can't

• introduced: 2.0.0

  introduced: 2.0.0

• introduced: pre-2009

  introduced: pre-2009

• introduced: pre-2012

  introduced: pre-2012

• introduced: pre-2017

  introduced: pre-2017

• introduced: v1.9.7

  introduced: v1.9.7