-
Notifications
You must be signed in to change notification settings - Fork 256
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.
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
Facilitate integration of Dafny into larger projects #5206
Comments
To the end of this issue, I have created lorrel-py. I haven't done much yet, but I would recommend doing something similar for the other supported back-end languages. I would also invite discussion here and PRs for lorrel-py for discussion and suggestions. |
Hi Alex! Thanks very much for taking the time to write this up, and for the enthusiasm to push for this improvement! This deserves some deeper discussion, but let me at least respond to your points and provide some background on the current status and what's already in the works:
I do agree it would be great to have a full example of integration for each target language. What we do have is some great examples of building Dafny code into reusable libraries in other languages, which can then obviously be used in other code bases without even being aware of Dafny, thanks to the AWS Crypto Tools team:
Even then, those projects are designed to be multi-target libraries, where the priority is supporting integration with many different langauges from the same code base. It is also worthwhile to shoot for easy integration of Dafny into existing code bases in a single language at a time as easily as possible, although the language and tooling support for both cases will definitely overlap.
We're definitely on top of this!
Still need to publish the runtimes in the other languages but that's on the backlog. But I think you're right that the documentation could emphasize the use case of translating Dafny to other target languages more, which would make it more obvious.
It absolutely is. |
Hey Robin! Thank you for the detailed reply!
I took a look through the linked repositories, and I can't really discern how one would use those as a jumping off point for their own integration of Dafny into their project. From what I can tell, those are really designed to fit into a larger AWS ecosystem (I'm not personally very savvy for AWS technologies). So, in-line with creating examples in the different target languages, I think I may be able to make a pretty strong example for Python and start one for C++. I'm not very proficient in project wrangling for any of the other target languages (I've used C#, but only here and for Unity).
Excellent! I was misled by #3127, so I appreciate you closing that out. In my endeavors for working through my own attempt at integrating Dafny into a larger Python project, I have identified a couple of findings. I will the most apparent ones here, and then we can decide if they should be split into different issues or not. Findings:
import sys
from typing import Callable, Any, TypeVar, NamedTuple
from math import floor
from itertools import count
import module_
import _dafny
import System_
# Module: module_
class default__:
def __init__(self):
pass
@staticmethod
def add(x, y):
return (x) + (y)
I have some sizable roadblock for the "actual" example of integration of Dafny into a larger project, thus I will focus my future efforts into making an "ideal" example. After the "ideal" example is established, I will ask for help in what it would take using the current implementation model to generate the same or similar result. As a side note, linters complain a lot about the generated Python code. This would further complicate integration into other build processes since all of the generated files would essentially need to be ignored. |
I have finally fleshed out a prototype for Dafny integration into larger Python projects here. I would appreciate any time that can be taken to review what I have put together. |
Summary
Define detailed user stories and CONOPs for users who would like to use Dafny as a part of their larger code base.
Background and Motivation
Dafny supports various back-ends for things translation, compiling, and execution, but the current feature set seems to lack coherence and do not provide straightforward models of Dafny integration into larger code bases. For instance, when translating to Python, the documentation doesn't mention which version of Python is being targeted, nor does Dafny allow the user to specify such.
Proposed Feature
Establishing detailed user stories and acceptance tests for integration of Dafny into projects based on other languages. Specifically, and most importantly, I would propose creating example projects in each available back-end language that demonstrates how to incorporate Dafny code inside the parent code base.
I would propose an overhaul of the documentation concerning these activities.
I would propose publishing Dafny and the Dafny runtime in the package ecosystems for applicable languages. For instance, publishing Dafny on pypi.org for use in build systems, and publishing the Dafny runtime for use as a project dependency in those projects.
Proposal 1 takes the highest priority as it would inform the direction on proposals 2 and 3. Most importantly is figuring out how a user wants to use Dafny in their larger code base, then we can catch Dafny up to support that CONOPs.
Alternatives
The current model is technically workable, as such this proposal should be considered an enhancement to improve adoptability of Dafny, not necessarily to improve its performance or core feature set (unless use in other languages is considered a core feature).
The text was updated successfully, but these errors were encountered: