Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix(deps): update dependency org.dafny:dafnyruntime to v4.8.0 #866

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix(deps): update dependency org.dafny:dafnyruntime to v4.8.0 #866

wants to merge 1 commit into from

Conversation

mend-for-github-com[bot]
Copy link
Contributor

@mend-for-github-com mend-for-github-com bot commented Sep 8, 2024 •
edited
Loading

This PR contains the following updates:

Package Change Age Adoption Passing Confidence
org.dafny:DafnyRuntime 4.2.0 -> 4.8.0 age adoption passing confidence

Release Notes

dafny-lang/dafny (org.dafny:DafnyRuntime)

v4.8.0

New features

  • Introduce hide statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. Hide statements make the opaque keyword on functions obsolete. (https://github.com/dafny-lang/dafny/pull/5562)

  • Let the command measure-complexity output which verification tasks performed the worst in terms of resource count. Output looks like:
    ...
    Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources
    Verification task on line 7 in file measure-complexity.dfy consumed 9065 reshttps://github.com/dafny-lang/dafny/pull/5631lang/dafny/pull/5631)

  • Enable the option --enforce-determinism for the commands resolve and verify (https://github.com/dafny-lang/dafny/pull/5632)

  • Method calls get an optional by-proof that hides the precondtion and its proof (https://github.com/dafny-lang/dafny/pull/5662)

Bug fixes

v4.7.0

New features

  • Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow.

  • Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion. (https://github.com/dafny-lang/dafny/pull/5281)

  • Support newtypes based on map and imap (https://github.com/dafny-lang/dafny/pull/5175)

  • To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to --library. When using dafny verify, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag --dont-verify-dependencies. (https://github.com/dafny-lang/dafny/pull/5297)

  • Experimental Dafny-to-Rust compiler development

  • Allow for plugins to add custom request handlers to the language server. (https://github.com/dafny-lang/dafny/pull/5161)

  • Deprecated the unicode-char option (https://github.com/dafny-lang/dafny/pull/5302)

  • Warn when passing a Dafny source file to --library (https://github.com/dafny-lang/dafny/pull/5313)

  • Add support for "translation records", which record the options used when translating library code.

    • --translation-record - Provides a .dtr file from a previous translation of library code. Can be specified multiple times.
    • --translation-record-output - Customizes where to write the translation record for the current translation. Defaults to the output directory.
      Providing translation records is necessary to handle options such as --outer-module that affect how code is translated.
      https://github.com/dafny-lang/dafny/pull/5346ull/5346)

  • The new decreases to expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (https://github.com/dafny-lang/dafny/pull/5367)

  • The new assigned expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (https://github.com/dafny-lang/dafny/pull/5501)

  • Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript.

  • Introduce additional warnings that previously only appeared when running the dafny audit command. Two warnings are as follows:

    • Emit a warning when exporting a declaration that has requires clauses or subset type inputs
    • Emit a warning when importing a declaration that has ensures clauses or subset type outputs
      Those two can be silenced with the flag --allow-external-contracts. A third new warning occurs when using bodyless functions marked with {:extern}, and can be silenced using the option --allow-external-function.

  • Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual.

Bug fixes

v4.6.0

New features

Bug fixes

v4.5.0

New features

  • Add the option --include-test-runner to dafny translate, to enable getting the same result as dafny test when doing manual compilation. (https://github.com/dafny-lang/dafny/pull/3818)

    • Fix: verification in the IDE no longer fails for iterators
    • Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
    • Fix: let the IDE correctly use the solver-path option when it's specified in a project file
    • Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program.
      https://github.com/dafny-lang/dafny/pull/4798ull/4798)
    • Add an option --filter-position to the dafny verify command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, dafny verify dfyconfig.toml --filter-position=source1.dfy:5 will only verify things that range over line 5 in the file source1.dfy. In combination with ``--isolate-assertions, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: dafny verify MyFile.dfy --filter-position=:23`
    • Add an option --filter-symbol to the dafny verify command, that only verifies symbols whose fully qualified name contains the given argument. For example, dafny verify dfyconfig.toml --filter-symbol=MyModule will verify everything inside MyModule.
    • The option --boogie-filter has been removed in favor of --filter-symbol
      https://github.com/dafny-lang/dafny/pull/4816ull/4816)

  • Add a json format to those supported by --log-format and /verificationLogger, for producing thorough, machine readable logs of verification results. (https://github.com/dafny-lang/dafny/pull/4951)

    • Flip the behavior of --warn-deprecation and change the name to --allow-deprecation, so the default is now false, which is standard for boolean options.
    • When using --allow-deprecation, deprecated code is shown using tooltips in the IDE, and on the CLI when using --show-tooltips.
    • Replace the option --warn-as-error with the option --allow-warnings. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous --warn-as-error option, warnings are always reported as warnings.
      • During development, users must use dafny run --allow-warnings if they want to run their Dafny code when it contains warnings.
      • If users have builds that were passing with warnings, they have to add --allow-warnings to allow them to still pass.
      • If users upgrade to a new Dafny version, and are not using --allow-warnings, and do not want to migrate off of deprecated features, they will have to use --allow-deprecation.
    • When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
    • A doo file that was created using --allow-warnings causes a warning if used by a consumer that does not use it.
      https://github.com/dafny-lang/dafny/pull/4971ull/4971)

  • The new {:contradiction} attribute can be placed on an assert statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when --warn-contradictory-assumptions is turned on. (https://github.com/dafny-lang/dafny/pull/5001)

  • Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (https://github.com/dafny-lang/dafny/pull/5032)

  • Under the CLI option --general-newtypes, the base type of a newtype declaration can now be (int or real, as before, or) bool, char, or a bitvector type.

    as and is expressions now support more types than before. In addition, run-time type tests are supported for is expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both as and is allow many more useful cases than before, using --general-newtypes will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the as/is via int.
    https://github.com/dafny-lang/dafny/pull/50615061)

  • Allow newtype declarations to be based on set/iset/multiset/seq. (https://github.com/dafny-lang/dafny/pull/5133)

Bug fixes

v4.4.0

New features

  • Reads clauses on method declarations are now supported when the --reads-clauses-on-methods option is provided.
    The {:concurrent} attribute now verifies that the reads and modifies clauses are empty instead of generating an auditor warning.
    https://github.com/dafny-lang/dafny/pull/44404440)

  • Added two new options, --warn-contradictory-assumptions and --warn-redundant-assumptions, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (https://github.com/dafny-lang/dafny/pull/4542)

  • Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (https://github.com/dafny-lang/dafny/pull/4563)

  • Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/4619)

  • The new --verification-coverage-report flag to dafny verify creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for dafny generate-tests --coverage-report and files from the two commands can be merged. (https://github.com/dafny-lang/dafny/pull/4625)

  • Built-in types such as the nat subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
    instead of emitted on every call to dafny translate, to avoid potential duplicate definitions when translating components separately.
    https://github.com/dafny-lang/dafny/pull/46584658)

  • The new --only-label option to merge-coverage-reports includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option --only-label NotCovered will highlight only the regions not covered by either testing or verification. (https://github.com/dafny-lang/dafny/pull/4673)

  • The Dafny distribution now includes standard libraries, available with the --standard-libraries option.
    See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for detailhttps://github.com/dafny-lang/dafny/pull/4678ull/4678)

  • Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/4681)

  • The new --coverage-report flag to dafny run and dafny test creates an HTML report highlighting which portions of the program were executed at runtime. (https://github.com/dafny-lang/dafny/pull/4755)

  • Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute {:disable-nonlinear-arithmetic},
    which optionally takes the value false to enable nonlinear arithmetihttps://github.com/dafny-lang/dafny/pull/4773ull/4773)

  • Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (https://github.com/dafny-lang/dafny/pull/4855)

Bug fixes

Configuration

📅 Schedule: Branch creation - At any time (no schedule defined), Automerge - At any time (no schedule defined).

🚦 Automerge: Disabled by config. Please merge this manually once you are satisfied.

♻ Rebasing: Whenever PR becomes conflicted, or you tick the rebase/retry checkbox.

🔕 Ignore: Close this PR and you won't be reminded about this update again.

  • If you want to rebase/retry this PR, check this box

@github-actions github-actions bot added the backport 2.x backport PRs to 2.x branch label Sep 8, 2024
@mend-for-github-com
fix(deps): update dependency org.dafny:dafnyruntime to v4.8.0
525c9b5 
Signed-off-by: mend-for-github-com[bot] <mend-for-github-com[bot]@users.noreply.github.com>
@mend-for-github-com mend-for-github-com bot force-pushed the whitesource-remediate/org.dafny-dafnyruntime-4.x branch from 2eed6e7 to 525c9b5 Compare September 10, 2024 15:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dbwiddis dbwiddis dbwiddis approved these changes

@owaiskazi19 owaiskazi19 Awaiting requested review from owaiskazi19 owaiskazi19 is a code owner

@joshpalis joshpalis Awaiting requested review from joshpalis joshpalis is a code owner

@ohltyler ohltyler Awaiting requested review from ohltyler ohltyler is a code owner

@amitgalitz amitgalitz Awaiting requested review from amitgalitz amitgalitz is a code owner

@jackiehanyang jackiehanyang Awaiting requested review from jackiehanyang jackiehanyang is a code owner

At least 2 approving reviews are required to merge this pull request.

Assignees
No one assigned
Labels
backport 2.x backport PRs to 2.x branch skip-changelog
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@dbwiddis