Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / dafny-lang/dafny issues and pull requests

#5164 - Remove experimental warning on `--type-system-refresh`

Issue - State: open - Opened by robin-aws 7 months ago
Labels: kind: enhancement, release-blocker

#5163 - Remove fragile .expect file that doesn't test much

Pull Request - State: closed - Opened by atomb 7 months ago
Labels: run-deep-tests

#5163 - Remove fragile .expect file that doesn't test much

Pull Request - State: closed - Opened by atomb 7 months ago
Labels: run-deep-tests

#5162 - Use Boogie v3.1.2

Pull Request - State: closed - Opened by atomb 7 months ago

#5162 - Use Boogie v3.1.2

Pull Request - State: open - Opened by atomb 7 months ago

#5160 - Stuck in verification

Issue - State: open - Opened by MikaelMayer 7 months ago - 7 comments
Labels: kind: enhancement, incompleteness

#5160 - Stuck in verification

Issue - State: open - Opened by MikaelMayer 7 months ago - 5 comments
Labels: kind: enhancement, incompleteness

#5159 - More random seed logging

Pull Request - State: open - Opened by keyboardDrummer 7 months ago

#5159 - More random seed logging

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago

#5158 - Option to run tests for only certain backends

Issue - State: open - Opened by alexporter8013 7 months ago
Labels: kind: enhancement

#5157 - Error message on exception during verification

Pull Request - State: open - Opened by atomb 7 months ago

#5157 - Error message on exception during verification

Pull Request - State: closed - Opened by atomb 7 months ago - 1 comment

#5156 - Crash on running a program on the library backend

Issue - State: open - Opened by robin-aws 7 months ago - 1 comment
Labels: kind: bug, crash

#5156 - Crash on running a program on the library backend

Issue - State: open - Opened by robin-aws 7 months ago - 1 comment
Labels: kind: bug, crash

#5155 - ESDK and DB ESDK nightly builds broken

Issue - State: open - Opened by robin-aws 7 months ago - 1 comment

#5154 - Dafny hangs when verifying certain code

Issue - State: open - Opened by atomb 7 months ago
Labels: kind: bug, release-blocker

#5154 - Dafny hangs when verifying certain code

Issue - State: closed - Opened by atomb 7 months ago
Labels: kind: bug, release-blocker

#5153 - Fix Cycle in type declaration causes crash (#4471)

Pull Request - State: closed - Opened by ssomayyajula 7 months ago

#5153 - Fix Cycle in type declaration causes crash (#4471)

Pull Request - State: open - Opened by ssomayyajula 7 months ago

#5152 - fix: Avoid NPE when building a doo file with —no-verify

Pull Request - State: closed - Opened by robin-aws 7 months ago

#5152 - fix: Avoid NPE when building a doo file with —no-verify

Pull Request - State: closed - Opened by robin-aws 7 months ago

#5151 - Resolution happens x4

Issue - State: open - Opened by MikaelMayer 7 months ago
Labels: kind: bug

#5150 - Add incremental verification progress reporting in a Dafny-centric way

Issue - State: closed - Opened by atomb 7 months ago - 2 comments
Labels: kind: enhancement

#5149 - Fix direction of library implication for --allow-warnings

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago - 1 comment

#5148 - Unable to Prove Object Unchanged After Unrelated Method Call

Issue - State: open - Opened by whonore 7 months ago
Labels: incompleteness

#5147 - Draft: Fix #4127 Too many parens for Python

Pull Request - State: open - Opened by alexporter8013 7 months ago

#5145 - StandardLibraries fail to load with `--allow-warnings` flag and throw NPE

Issue - State: closed - Opened by ShubhamChaturvedi7 7 months ago - 2 comments
Labels: kind: bug

#5144 - Type mismatch allowed in ensures clause with type parameters and datatypes

Issue - State: open - Opened by atomb 7 months ago - 4 comments
Labels: kind: bug, during 3: execution of incorrect program

#5143 - Exception when generating doo file with `--no-verify` flag

Issue - State: closed - Opened by ShubhamChaturvedi7 7 months ago - 1 comment
Labels: kind: bug, release-blocker, priority: next

#5141 - docs: remove `polyfill.io` in the toc page

Pull Request - State: closed - Opened by SukkaW 7 months ago - 2 comments

#5140 - Go libray module support

Pull Request - State: open - Opened by ShubhamChaturvedi7 7 months ago - 13 comments

#5139 - chore: Rename adjustment to refinement

Pull Request - State: closed - Opened by RustanLeino 7 months ago - 1 comment

#5138 - Fix measure-complexity command

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago - 1 comment

#5137 - move: Split ResolutionErrors.dfy into 10 smaller files

Pull Request - State: closed - Opened by RustanLeino 7 months ago

#5137 - move: Split ResolutionErrors.dfy into 10 smaller files

Pull Request - State: closed - Opened by RustanLeino 7 months ago

#5136 - Empty type initialization leads to proving false

Issue - State: open - Opened by MikaelMayer 7 months ago - 4 comments
Labels: kind: bug, part: verifier, priority: next, during 3: execution of incorrect program

#5135 - Support Counterexamples with New CLI Interface

Pull Request - State: open - Opened by Dargones 7 months ago - 1 comment
Labels: part: counterexamples

#5135 - Support Counterexamples with New CLI Interface

Pull Request - State: closed - Opened by Dargones 7 months ago - 1 comment
Labels: part: counterexamples

#5134 - Judging by the current code --iterations option is ignored

Issue - State: closed - Opened by keyboardDrummer 7 months ago - 4 comments
Labels: kind: bug, release-blocker

#5133 - feat: newtype for (non-map) collection types

Pull Request - State: closed - Opened by RustanLeino 7 months ago

#5132 - Error documentation improvement

Issue - State: closed - Opened by MikaelMayer 7 months ago
Labels: area: error-reporting

#5131 - Dafny gets stuck - Server process exited with code 0

Issue - State: open - Opened by Timmmm 7 months ago - 5 comments
Labels: kind: bug, part: language server, priority: next, during 2: compilation of correct program

#5130 - Code completion request causes exception

Issue - State: open - Opened by keyboardDrummer 7 months ago
Labels: kind: bug, part: language server, during 1: program development

#5129 - The opaque keyword does not always hide the body of functions

Issue - State: open - Opened by keyboardDrummer 7 months ago - 6 comments
Labels: kind: bug, part: verifier, during 1: program development

#5128 - Adds support for Go module name

Pull Request - State: closed - Opened by ShubhamChaturvedi7 7 months ago - 1 comment

#5127 - Use Tasks for running processes

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago

#5126 - measure-complexity non-deterministic?

Issue - State: open - Opened by hmijail 7 months ago - 17 comments
Labels: kind: bug, priority: next, part: tools, during 1: program development

#5124 - Exception in SchorrWaite.dfy is not caught by tests

Issue - State: closed - Opened by keyboardDrummer 7 months ago
Labels: release-blocker

#5123 - Improve exception handling

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago - 1 comment

#5121 - Add missing Unsupported Feature exception for Rust

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago - 1 comment

#5120 - Check for mistyped options when using `dafny run`

Pull Request - State: closed - Opened by keyboardDrummer 7 months ago

#5119 - Fix cloning bug

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago

#5118 - Add translation was aborted message

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago - 2 comments

#5117 - Warnings in the code neither generate any output nor any errors

Issue - State: closed - Opened by ShubhamChaturvedi7 8 months ago - 3 comments
Labels: kind: bug, release-blocker, part: CLI

#5117 - Warnings in the code neither generate any output nor any errors

Issue - State: closed - Opened by ShubhamChaturvedi7 8 months ago - 3 comments
Labels: kind: bug, release-blocker, part: CLI

#5116 - move: Move BoundedPool classes into separate folder

Pull Request - State: closed - Opened by RustanLeino 8 months ago

#5115 - chore: Rename EmitIsRuneTest to EmitIsUnicodeScalarValueTest

Pull Request - State: closed - Opened by RustanLeino 8 months ago

#5114 - Rewrite `check-examples` so it uses C# instead of bash

Issue - State: open - Opened by keyboardDrummer 8 months ago
Labels: kind: language development speed

#5114 - Rewrite `check-examples` so it uses C# instead of bash

Issue - State: open - Opened by keyboardDrummer 8 months ago - 1 comment
Labels: kind: language development speed

#5113 - Allow moving errorId code around in the codebase.

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago

#5113 - Allow moving errorId code around in the codebase.

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago

#5112 - Replace MakeErrorCatalog.java

Issue - State: open - Opened by keyboardDrummer 8 months ago
Labels: kind: language development speed, priority: next

#5112 - Replace MakeErrorCatalog.java

Issue - State: closed - Opened by keyboardDrummer 8 months ago - 1 comment
Labels: kind: language development speed, priority: next

#5110 - Make `dafny verify` more consistent

Pull Request - State: open - Opened by keyboardDrummer 8 months ago

#5110 - Make `dafny verify` more consistent

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago - 3 comments

#5109 - docs: Link to the _brittle_ section

Pull Request - State: closed - Opened by kazarmy 8 months ago

#5108 - Use CliCompilation instead of SynchronousCliCompilation for all commands

Issue - State: open - Opened by keyboardDrummer 8 months ago
Labels: kind: language development speed

#5108 - Use CliCompilation instead of SynchronousCliCompilation for all commands

Issue - State: open - Opened by keyboardDrummer 8 months ago
Labels: kind: language development speed

#5107 - Translate only recognized attributes

Pull Request - State: closed - Opened by atomb 8 months ago

#5107 - Translate only recognized attributes

Pull Request - State: closed - Opened by atomb 8 months ago

#5106 - Duplicate: Lambda `requires` clauses intentionally opaque?

Issue - State: closed - Opened by racko 8 months ago - 4 comments
Labels: kind: enhancement

#5106 - Lambda `requires` clauses intentionally opaque?

Issue - State: open - Opened by racko 8 months ago - 2 comments
Labels: kind: enhancement

#5105 - Bump Boogie to v3.0.12

Pull Request - State: closed - Opened by atomb 8 months ago

#5105 - Bump Boogie to v3.0.12

Pull Request - State: closed - Opened by atomb 8 months ago

#5103 - Update documentation for --filter-position

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago

#5102 - Enable Dafny CLI to easily measure brittleness

Issue - State: open - Opened by keyboardDrummer 8 months ago - 4 comments
Labels: kind: enhancement, misc: instability

#5100 - Major 4.4 verification regression

Issue - State: closed - Opened by ajewellamz 8 months ago - 6 comments
Labels: kind: bug, area: performance, part: verifier, misc: instability

#5099 - Fix some typos in `docs/DafnyRef/README.md`

Pull Request - State: closed - Opened by kazarmy 8 months ago - 1 comment

#5098 - Compute prefix lemmas earlier in the resolution pipeline

Pull Request - State: closed - Opened by RustanLeino 8 months ago - 1 comment

#5097 - dafny run file.dfy --include file.cs does not raise errors

Issue - State: closed - Opened by MikaelMayer 8 months ago - 9 comments
Labels: kind: bug, makes-mikael-grateful

#5096 - Fix "assertion batch" anchor

Pull Request - State: closed - Opened by kazarmy 8 months ago - 1 comment

#5095 - Subtraction of non-native type is not yet supported in C++ backend - BigNumber issue

Issue - State: closed - Opened by shenweihai1 8 months ago - 4 comments
Labels: kind: bug

#5094 - Stack Overflow with Long Verbatim String

Issue - State: open - Opened by whonore 8 months ago
Labels: kind: bug, priority: not yet, during 2: compilation of correct program

#5092 - Malformed Python code for some functions involving lambdas

Issue - State: closed - Opened by fabiomadge 8 months ago - 2 comments
Labels: kind: bug, part: code-generation, lang: python, priority: next, during 2: compilation of correct program

#5091 - Idea (integration tests): replace .expect files with inline expected error message comments

Issue - State: open - Opened by robin-aws 8 months ago
Labels: kind: enhancement, kind: language development speed

#5090 - Remove boogie filter

Pull Request - State: closed - Opened by keyboardDrummer 8 months ago

#5089 - Recursively defined datatype can lead to NPE in Java

Issue - State: closed - Opened by robin-aws 8 months ago - 2 comments
Labels: kind: bug, priority: next, during 4: execution of correct program

#5088 - Hang with `dafny verify` on `Std`

Issue - State: open - Opened by atomb 8 months ago - 5 comments
Labels: kind: bug, during 2: compilation of correct program

#5085 - Replace `docs/HowToFAQ/MakeErrorCatalog.java` with something more robust

Issue - State: open - Opened by keyboardDrummer 8 months ago
Labels: kind: language development speed