debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
*	Implement 'extern' declaration modifier.	Richard L. Ford	2016-01-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed.
*	VS IDE performance - invoke dafny parser when the buffer hasn't changed for	qunyanm	2016-01-20
\| \| \| \| \| \|	half a second, but delay calling Dafny resolver until the text buffer hasn't been changed for 5 seconds. Also save the parsing result from TokenTagger in ITextBuffer's property instead of in a static field.
*	DafnyExtension: Add menu item for automatic induction (mainly developed by ↵	wuestholz	2015-10-26
\| \| \| \|	Rustan).
*	Make /autoTriggers:1 be the default in Visual Studio	leino	2015-10-24
\|
*	Enable unicode output in the VS extension	Clément Pit--Claudel	2015-08-19
\|
*	Refactor the error reporting code	Clément Pit--Claudel	2015-08-18
\| \| \| \| \|	The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
*	Tiny refactoring in the extension's driver	Clément Pit--Claudel	2015-07-31
\|
*	Update the VS extension to use the error interface defined in 576eac2e17ff	Clément Pit--Claudel	2015-07-29
\|
*	Update DafnyExtension to use the parser constructor introduced in d2e394fc4b93	Clément Pit--Claudel	2015-07-24
\|
*	Fix: Visual studio did not show warnings.	Clément Pit--Claudel	2015-07-23
\| \| \| \| \|	To check if the fix works, try declaring a static top level function. Initial work on this patch by Rustan
*	DafnyExtension: Added experimental support for diagnosing timeouts.	wuestholz	2015-05-18
\|
*	Add DafnyOptions.txt, and have the Dafny Visual Studio extension read ↵	chrishaw	2015-03-11
\| \| \| \|	command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.
*	DafnyExtension: Made it use the more advanced on-demand re-verification by ↵	wuestholz	2015-01-26
\| \| \| \|	default.
*	Ensure that no file is processed twice, even if one command-line file is ↵	Bryan Parno	2014-10-27
\| \| \| \|	included by another command-line file.
*	DafnyExtension: Fixed minor issue in the menu.	wuestholz	2014-10-19
\|
*	Did more refactoring.	wuestholz	2014-09-23
\|
*	DafnyExtension: minor change	wuestholz	2014-09-22
\|
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-09
\|
*	Merge	Dan Rosén	2014-07-07
\|\
\| *	Minor change due to change in Boogie	wuestholz	2014-06-28
\| \|
\| *	DafnyExtension: Made it possible to activate the more advanced verification ↵	wuestholz	2014-06-23
\| \| \| \| \| \| \| \|	result caching in Boogie (experimental for now).
* \|	DafnyExtension: Minor change to deal with a change in the Boogie ↵	wuestholz	2014-06-20
\| \| \| \| \| \| \| \|	command-line options
\| *	DafnyExtension: Minor change to deal with a change in the Boogie ↵	wuestholz	2014-06-20
\| \| \| \| \| \| \| \|	command-line options
* \|	Fixed issues with absolute file names in the expected output for the lit tests.	wuestholz	2014-06-04
\| \|
\| *	Fixed issues with absolute file names in the expected output for the lit tests.	wuestholz	2014-06-04
\|/
*	DafnyExtension: Made it display the compilation output in the VS output pane.	wuestholz	2014-04-21
\|
*	DafnyExtension: Reduce the default number of Z3 instances by one.	wuestholz	2013-12-26
\|
*	Add support for the "include" keyword, which accepts a (possibly relative) path	Bryan Parno	2013-12-10
\| \| \| \| \|	to another Dafny file. That file's functions and methods are included but not checked. This is intended to support incremental verification on a per-file basis.
*	Fix some things due to changes in Boogie (execution engine API, ↵	wuestholz	2013-12-09
\| \| \| \|	'UnivBackPred2.smt2' no longer needed).
*	DafnyExtension: Did some refactoring to integrate the Dafny menu more tightly.	wuestholz	2013-07-28
\|
*	DafnyExtension: Added support for collecting additional information during ↵	wuestholz	2013-07-15
\| \| \| \|	resolution and displaying it.
*	DafnyExtension: Enabled model extraction for verification failures.	wuestholz	2013-07-12
\|
*	Did some refactoring of the interaction with the Boogie execution engine.	wuestholz	2013-07-10
\|
*	DafnyExtension: Integrated support for multiple Z3 instances in Boogie ↵	wuestholz	2013-07-09
\| \| \| \|	(incl. request cancellation).
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-24
\|
*	DafnyExtension: Made it display verification errors incrementally.	wuestholz	2013-06-20
\|
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-19
\|
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-19
\|
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-19
\|
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-18
\|
*	Did some refactoring of the error reporting functionality.	wuestholz	2013-06-18
\|
*	DafnyExtension: Fixed an issue in the verification result caching.	wuestholz	2013-06-17
\|
*	DafnyExtension: Disabled the default console printer for Boogie.	wuestholz	2013-06-13
\|
*	DafnyExtension: Added a menu item to toggle verification result caching.	wuestholz	2013-06-12
\|
*	DafnyExtension: Added a todo.	wuestholz	2013-06-12
\|
*	DafnyExtension: Did some refactoring.	wuestholz	2013-06-11
\|
*	DafnyExtension: Did some refactoring.	wuestholz	2013-06-11
\|
*	DafnyExtension: Did some refactoring.	wuestholz	2013-06-10
\|
*	DafnyExtension: Improved the way errors (incl. locations) are kept up-to-date.	wuestholz	2013-06-10
\|
*	DafnyExtension: Worked on integrating the verification result caching.	wuestholz	2013-06-07
\|