debian-dafny - Debian packaging for Dafny

	Commit message (Collapse)	Author	Age
...
*	Merge	Dan Rosén	2014-08-11
\|\
* \|	Add higher-order-functions and some other goodies	Dan Rosén	2014-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
\| *	Merge	leino	2014-08-02
\| \|\
\| * \|	Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵	leino	2014-08-02
\|/ / \| \| \| \| \| \|	the resolver and translator
\| *	added trait feature:	Reza Ahmadi	2014-07-18
\|/ \| \| \| \| \|	-possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
*	Fixed build break from recent change	leino	2014-07-15
\|
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-10
\|
*	Worked on the more advanced verification result caching.	wuestholz	2014-07-09
\|
*	Build VS Extension for both VS 2012 and VS 2013.	Rustan Leino	2014-07-08
\| \| \| \|	Currently builds only in VS 2012. To build in VS 2013, change MinimumVisualStudioVersion from 11.0 to 12.0 in these two .csproj files.
*	Merge	Dan Rosén	2014-07-07
\|\
\| *	DafnyExtension: Worked on adding support for Visual Studio 2013.	wuestholz	2014-07-02
\| \|
\| *	Dispose DafnyTokenTagger	Rustan Leino	2014-07-01
\| \|
\| *	Color nested comments correctly in the Dafny IDE	Rustan Leino	2014-07-01
\| \|
\| *	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: Added some support for logging program snapshots that are ↵	wuestholz	2014-04-21
\| \| \| \|	sent to the verifier.
*	Run-time real support	Rustan Leino	2014-04-13
\|
*	Added "modify" statement.	Rustan Leino	2014-04-03
\| \| \| \|	In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
*	DafnyExtension: Fixed a concurrency issue.	wuestholz	2014-04-03
\|
*	Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵	Rustan Leino	2014-03-17
\| \| \| \|	to VarDeclStmt.Locals
*	Fixed build-break typo	Rustan Leino	2014-02-23
\|
*	Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵	Rustan Leino	2014-02-23
\| \| \| \|	-> "prefix lemma")
*	Syntax highlighting for reals	Rustan Leino	2014-02-13
\|
*	Fixed bug in DafnyExtension (hover text computation would crash if ↵	Rustan Leino	2014-02-06
\| \| \| \| \| \|	Translator had not been run). Fixed duplicate hover text information for Lines of calc statements.
*	Mark auto-generated expressions (in "decreases" clauses) and don't use these ↵	Rustan Leino	2014-02-04
\| \| \| \|	when figuring out hover text.
*	Version 1.8.0.10115 release candidate	Rustan Leino	2014-01-15
\|
*	Manually adjusted merge	Rustan Leino	2014-01-08
\|
*	One more file to go with the previous check-in (DafnyRuntime.cs apparently ↵	Rustan Leino	2014-01-06
\| \| \| \|	gets copied)
*	DafnyExtension: Reduce the default number of Z3 instances by one.	wuestholz	2013-12-26
\|
*	Compute default decreases clauses in Resolver instead of in the Translator.	Rustan Leino	2013-12-19
\| \| \| \|	Make this information available as AdditionalInformation, that is, as hover text in the IDE.
*	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).
*	Fixed build failures due to changes in Boogie.	wuestholz	2013-11-23
\|
*	Removed old keyword "choose"	Rustan Leino	2013-08-06
\|
*	Bumped version to 1.7.0, to be released as a binary and on rise4fun.	wuestholz	2013-08-06
\|
*	Updated 'PrepareDafnyZip.bat'.	wuestholz	2013-08-05
\|
*	DafnyExtension: Use the same version number as Dafny (unfortunately needs to ↵	wuestholz	2013-08-05
\| \| \| \|	be updated separately in the vsixmanifests).
*	DafnyExtension: Fixed issue with visual elements being accessed by ↵	wuestholz	2013-08-04
\| \| \| \|	non-owning thread.
*	DafnyExtension: Did some refactoring and added a description to error states.	wuestholz	2013-08-03
\|
*	Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵	Rustan Leino	2013-08-02
\| \| \| \|	a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
*	DafnyExtension: Fixed a minor issue in the error selection.	wuestholz	2013-08-01
\|
*	DafnyExtension: Fixed a minor issue in the error selection.	wuestholz	2013-08-01
\|
*	DafnyExtension: Made it select the last error state by default when an error ↵	wuestholz	2013-08-01
\| \| \| \|	is selected.
*	DafnyExtension: Made it display if a variable was updated in a given model ↵	wuestholz	2013-08-01
\| \| \| \|	state.
*	DafnyExtension: Added support for displaying values from the model as hover ↵	wuestholz	2013-07-30
\| \| \| \|	text.