Hi Brian,
This is an artefact I forgot to remove. Changeset dc36cd801694 should
correct this. I am sorry for any inconvenience.
Sascha
Brian Huffman wrote:
> After pulling from the repository this morning, and trying to rebuild
> Isabelle/HOL, I immediately get the following error:
>
> Bad
* References 'trace_simp' and 'debug_simp' have been replaced by
configuration options stored in the context. Enabling tracing
(the case of debugging is similar) in proofs works via
using [[trace_simp=true]]
Tracing is then active for all invocations of the simplifier
in subsequent goal refinem
* New testing tool "Mirabelle" for automated (proof) tools. Applies several
tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
in a theory. To be used in batch mode via "isabelle mirabelle".
This bug has already been fixed, see
http://isabelle.in.tum.de/repos/isabelle/rev/40a0760a00ea
Regards,
Sascha
Tjark Weber wrote:
> On Fri, 2009-08-21 at 19:19 +0200, Dennis Walter wrote:
> > The following proof works fine if "Quick&Dirty" is enabled, i.e. in
> > interactive mode. But if this
New proof method "smt" for a combination of first-order logic
with equality, linear and nonlinear (natural/integer/real)
arithmetic, and fixed-size bitvectors; there is also basic
support for higher-order features (esp. lambda abstractions).
It is an incomplete decision procedure based on external
SMT's timeout option is also measured in seconds, and this is the
case since its beginning. I found this a natural decision, and no one
has ever objected to it.
Sascha
Tobias Nipkow wrote:
> Unless I have a lapse of memory, the timeout specifications for s/h and
> Nitpick are also in seconds, po
How about providing a parse function "time_of_string" which turns
strings like "30s" or "15ms" into proper times, and possibly adding a
configuration option scheme for times (besides the existing bool, int
and string schemes)? It seems that this could and should be provided
be provided by the syst
Hi,
There exists a theorem called "induct" in HOL, which changes after
every datatype declaration. What is the rationale behind this
theorem? Is it required for a particular purpose or just a forgotten
remainder of previous tunings? Shouldn't this suprising behaviour be
eliminated? Note that e
Hi Steve,
An arbitrary development snapshot of Isabelle is not required to run
as expected, but many snapshots do. Since your question is related to
such an arbitray version of Isabelle, I took the freedom to move your
question to the developer list.
To solve your issue, could you please specify
Hi,
With changeset 3214c39777ab, the SMT solvers have been turned into
components.
As a consequence, the now obsolete environment variables
(in settings files) CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER should be
removed. This only applies if you have used the smt method so before.
Prior to their
Hi,
To all of you who already copied the SMT solvers (CVC3, Yices, or Z3)
from the TUM server: Please copy the files again, as I have just
updated them in connection with changeset fda8511006f9. Sorry for the
inconvenience.
Sascha
___
isabelle-dev mail
Hi,
Until March 11, Google is looking for mentoring organization for this
year's Summer of Code, a two-month period where students from all over
the world improve open source software/projects.
http://socghop.appspot.com/gsoc/program/home/google/gsoc2011
We might participate as project -- and
Hi,
We are in the process of applying as a mentoring organization for this
year's Google Summer of Code (SoC). Some 150 open-source
organizations and some thousand students take part in SoC every year
-- and Google announced to accept more organizations this year.
http://socghop.appspot.com/gs
The website for the project ideas is actually (note the hyphen instead
of the underscore):
http://isabelle.in.tum.de/gsoc-ideas.html
Thanks to Christian Sternagel for reporting this.
Please don't hesitate to submit project ideas,
Jasmin & Sascha
Sascha Boehme wrote:
> Hi,
>
Alexander Krauss wrote:
> On 03/22/2011 10:17 PM, Makarius wrote:
> >I also wonder about mirabelle -q, which produces strange messages in the
> >regular makeall setup:
> >
> >http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l134
> >
> >http://isabelle.in.
We are happy to announce that two students are participating in this
year's Google Summer of Code for Isabelle:
Peter Skočovský, working on "Isabelle/jEdit document browser and
various enhancements" and mentored by Makarius. Peter is studying in
the European Master's program in Computational Logi
Hi Clemens,
Please note that Z3's license explicitly allows distribution for
non-commercial purposes such as teaching, academic research or public
demonstrations. Although Isabelle's BSD-style license would allow
Isabelle to be applied to commercial applications, too, it still is a
research produ
Hi,
Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?
Here is a more concrete example. Assume there is a declaration such
as:
declare_foo name = ...
which declares "name" as some new foo-entity. For later reference,
the declared foo-entities are b
Hi Gerwin,
This is because by default the smt method tries to reconstruct the
proof of Z3. For bitvectors, however, there is currently no Z3 proof
reconstruction. You might want to invoke the smt method as an oracle:
lemma "(x :: 8 word) + x = 2 * x"
using [[smt_oracle]]
by smt
Chee
Hi,
When the JDK is not given in the PATH variable, the command "isabelle
jedit" may fail with
./build-jars: line 189: jar: command not found
This is at least the case for hg id 08c22e8ffe70.
The problem occurs with Cygwin where the JDK is provided as a
component in the Isabelle bundle
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option "z3_with_extensions". Minor
INCOMPATIBILITY.
_
Quoting Lars Noschinski :
On 04.06.2012 09:28, Sascha Boehme wrote:
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the
I am sure this is already in the pipeline. It seems that the
variable YICES_INSTALLED (and the analogue for other solvers)
should be mentioned in the documentation of sledgehammer (since
what is currently given as installation instructions in `isabelle
doc sledgehammer` of changeset 3060e63
Hi,
Zitat von Ond?ej Kun?ar :
But AVL-Trees were already broken in Isabelle's changeset
791157a4179a (ensured that rewr_conv rule t = "t == u" literally not
just modulo beta-eta) before Jasmin's changeset 34b0464d7eef. It
seems that the changeset fixing rewr_conv interacts with smt. There
more stable way. I'll need a bit
more time. Everything should be fixed by the end of the year.
Cheers,
Sascha
- Ursprüngliche Nachricht -
Von: Jasmin Christian Blanchette
Gesendet: 04.12.2012 15:07
An: Makarius
Cc: isabelle-dev Mailinglist; Sascha Boehme
Betreff: Re: [isabelle-dev] Sta
Sascha Boehme wrote:
Hi,
Zitat von Ond?ej Kun?ar :
But AVL-Trees were already broken in Isabelle's changeset
791157a4179a (ensured that rewr_conv rule t = "t == u" literally
not just modulo beta-eta) before Jasmin's changeset 34b0464d7eef.
It seems that the change
Hi,
It could have been caused by my commit last night. I am not sure what I did
wrong, though.
Cheers,
Sascha
- Ursprüngliche Nachricht -
Von: Christian Sternagel
Gesendet: 21.12.2012 04:08
An: isabelle-dev
Betreff: [isabelle-dev] Repository trouble
Dear all,
just now, when I tried
Hi,
Is anyone using Isabelle on Cygwin and has build an image for a recent
Isabelle changeset? Or is Isabelle regularly build under Cygwin on any of
the test machines?
I've installed Cygwin from scratch two days ago and downloaded Isabelle (hg
id 5b889b1b465b). When building Pure, the PolyML
*** HOL ***
* New proof method "argo" using the built-in Argo solver based on SMT
technology.
The method can be used to prove goals of quantifier-free propositional logic,
goals based on a combination of quantifier-free propositional logic with
equality,
and goals based on a combination of quant
29 matches
Mail list logo
