Gentoo Packages

Search

Install

Install this package:

emerge -a dev-lang/dafny

If the package is masked, you can unmask it using the autounmask tool or standard emerge options:

autounmask dev-lang/dafny

Or alternatively:

emerge --autounmask-write -a dev-lang/dafny

Package Information

Description:

Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Java, JavaScript or Go (more to come!), so it can integrate with your existing workflow. Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing. Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures. Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.

Homepage:

https://dafny.org/ https://github.com/dafny-lang/dafny/

License:

Apache-2.0 BSD-2 MIT

Versions

Metadata

Description

• Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Java, JavaScript or Go (more to come!), so it can integrate with your existing workflow. Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing. Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures. Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.

Maintainers

• Gentoo Dotnet Project (dotnet@gentoo.org) - Type: project

Upstream

• Bugs: https://github.com/dafny-lang/dafny/issues/
• Changelog: https://github.com/dafny-lang/dafny/releases/
• Remote IDs:
  • github: dafny-lang/dafny

<pkgmetadata>
	<maintainer type="project">
		<email>dotnet@gentoo.org</email>
		<name>Gentoo Dotnet Project</name>
	</maintainer>
	<longdescription>
    Dafny is a verification-ready programming language. As you type in your
    program, Dafny's verifier constantly looks over your shoulder, flags any
    errors, shows you counterexamples, and congratulates you when your code
    matches your specifications. When you're done, Dafny can compile your code
    to C#, Java, JavaScript or Go (more to come!), so it can integrate with
    your existing workflow. Dafny will give you assurance that your code meets
    the specifications you write, while letting you write both code and
    specifications in the Dafny programming language itself. Since verification
    is an integral part of development, it will thus reduce the risk of costly
    late-stage bugs that are typically missed by testing. Dafny has support for
    common programming concepts such as classes and trait inheritance,
    inductive datatypes that can have methods and are suitable for pattern
    matching, lazily unbounded datatypes, subset types e.g. for bounded
    integers, lambdas, and immutable and mutable data structures. Dafny also
    offers an extensive toolbox for mathematical proofs, such as unbounded and
    bounded quantifiers, calculational proofs, pre- and post-conditions,
    termination conditions, loop invariants, and read/write specifications.
  </longdescription>
	<upstream>
		<changelog>https://github.com/dafny-lang/dafny/releases/</changelog>
		<doc>https://dafny.org/latest/DafnyRef/DafnyRef</doc>
		<bugs-to>https://github.com/dafny-lang/dafny/issues/</bugs-to>
		<remote-id type="github">dafny-lang/dafny</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Warning] USE flag 'test' in ebuild 4.11.0 is not documented in metadata.xml
• [Error] Missing md5-cache for ebuild dafny-4.11.0

USE Flags

Manage flags for this package: euse -i <flag> -p dev-lang/dafny | euse -E <flag> -p dev-lang/dafny | euse -D <flag> -p dev-lang/dafny

Files

• dafny-3.12.0-DafnyRuntime-csproj.patch
• dafny-4.11.0-lit-config.patch

Manifest