Am 15.12.2014 um 17:48 schrieb Makarius :
> On Wed, 3 Dec 2014, Jasmin Christian Blanchette wrote:
>
>> Those interfaces were never very polished, nor documented (although I might
>> come to add a section to "isabelle doc datatypes" about the ML functions --
>>
Hi Chris,
> is there a reliable way to check - given the name of a type constructor - how
> many dead type parameters it has?
>
> I tried
>
> (case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of
>SOME sugar =>
> if BNF_Def.dead_of_bnf (#fp_bnf sugar) > 0 then
>error "..."
> ...
>
Hi Gerwin,
Am 27.11.2014 um 00:06 schrieb Gerwin Klein :
> I wonder if it would be feasible to create a regression test for interactive
> commands like find_theorems so this noticed earlier, but that is a different
> topic.
We have regression tests for a number of other interactive diagnosis c
Hi Makarius,
>> I would expect that if Jasmin's plugin manager is also used in the code
>> generator, it would be easy to implement plugin selection for code_datatype,
>> too.
>
> This should work out easily with the unified Plugin_Name and Plugin concept
> of
> http://isabelle.in.tum.de/repo
Hi Florian,
Thanks for your input.
>> 1. Increase the timeout from 3600 s to, e.g. 4800.
[...]
> So, (1) is my opinion.
Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, e4d540c0dd57).
Judging from the log file, it would appear to me that it's an instance of
multithreading divergenc
Hi again,
Am 17.09.2014 um 11:40 schrieb Jasmin Christian Blanchette
:
> 1. "HOL-Proofs" times out since September 14 on "at-poly-e". On September 13,
> we had
>
>Timing HOL-Proofs (2 threads, 3161.882s elapsed time, 2889.329s cpu time,
> 840.167s GC t
Hi all,
The good news is that the port to the new datatypes have been overall a
success. There are only a handful of "old_datatype"s left in the AFP, and they
will go away as soon as Dmitriy gets a chance to fix a bug in his code
(presumably once he's back from vacation). Also good news: Timing
Hi Florian,
Am 10.09.2014 um 10:22 schrieb Florian Haftmann
:
> when we started this hook business, the situation was as follows:
>
> a) Hook clients were all for adding type class instances, i.e.
> inherently working a the theory level.
>
> b) Hooks were a bootstrap device, e.g. after a certa
Hi all,
It appears that the Sum of Squares server is down. This makes the build of the
"HOL-Library" session diverge, at least on my machine, when
"ISABELLE_FULL_TESTS" is enabled. In addition, it appears to be at the source
of the Isatest failures on "mac-poly-M4" and "mac-poly-M8". What's the
Am 09.09.2014 um 20:30 schrieb Jasmin Christian Blanchette
:
> So don't worry if your favorite theory gets some "datatype_new"s in them.
> They will go away soon enough.
I would like to add one thing: I am of course keeping an eye on Isatest and
Testboard. As usual, I w
Hi all,
As announced at last week's weekly meeting in Munich, I expect to perform the
following renamings in the coming weeks:
datatype ~> old_datatype
datatype_new ~> datatype
As a first step, I am manually changing lots of "datatype"s into
"datatype_new"s and ironing out the issues t
Hi all,
Dmitriy wrote:
>> Second question: is it considered "bad form" to rely on default rules?
> No, I think it's fine. Such (radical) changes of definitions (set in this
> case) are seldom.
I would like to add that this "radical" change broke only a handful of proofs
in the AFP, i.e., it wa
Hi all,
The "interpretation" mechanism, as defined in "Pure/interpretation.ML", is used
in a few places in Isabelle, including the new (co)datatype package, for
allowing other tools and users to register their hooks. Unfortunately, it works
at the theory level, which interacts poorly with local
* Old and new SMT modules:
- The old 'smt' method has been renamed 'old_smt' and moved to
'src/HOL/Library/Old_SMT.thy'. It provided for compatibility, until
applications have been ported to use the new 'smt' method. For the
method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0)
Hi Chris,
> consider the following datatype specification
>
> datatype_new 'f f =
>F1 'f 'f 'f 'f |
>F2 'f 'f 'f 'f
>
> (which takes about 1 second with Isabelle2014-RC0) does not terminate within
> a few minutes anymore.
> I did not have time to do a proper bisect until now. Maybe yo
Dear Leo,
Am 04.07.2014 um 07:48 schrieb Leo Freitas :
> Sledgehammering...
> "z3": The generated problem is malformed. Please report this to the Isabelle
> developers.
>
> I wasn’t sure whether the cast I was making for the shift operation was right
> or not, but anyhow I thought to send it
Am 07.07.2014 um 11:38 schrieb Makarius :
> You probably mean the defaults for the "Provers" in the Sledgehammer panel.
> It is now a bit simpler in only providing some static default, which is made
> persistent on the editor side if you change that.
>
> Adding "smt" there includes that prover
Hi Leo,
Am 04.07.2014 um 07:48 schrieb Leo Freitas :
> I was playing with HOL-Word to see if I could bring some discharged VCs from
> another tool into Isabelle.
> When I tried sledgehammer on it I got the error message for Z3
Thanks for the report! We will look into this. It may take some time
Am 01.07.2014 um 19:45 schrieb Makarius :
> * src/HOL/Tools/ATP/atp_problem_generate.ML
>
>Two occurrences that are not immediately clear. Looks like plain
>structural equality could do the job.
Right. This looks like very minor optimizations. I'm taking them out (pushed to
testboard
Am 01.07.2014 um 22:33 schrieb Makarius :
> One round of manual bisection yields the following, within the usual margin
> of error:
>
> changeset: 57470:9512b867259c
> user:blanchet
> date:Tue Jul 01 16:49:25 2014 +0200
> summary: fixed soundness bug in monotonicity-based t
Hi René,
> I have an unexpected problem when defining a datatype using datatype_new.
>
> theory Test
> imports
> "$AFP/Collections/ICF/impl/RBTSetImpl"
> begin
> datatype_new ('a,'b) bar = Foo 'a "'b option" "'b rs"
...
> Just wanting to report this,
Thank you for your report. This is now fix
- MaSh and MeSh are now used by default together with the traditional
MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
system option in Plugin Options / Isabelle / General to "none". Other
allowed values include "sml" (for the default SML engine) and "py"
- MaSh and MeSh are now used by default together with the traditional
MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
system option in Plugin Options / Isabelle / General to "none". Other
allowed values include "sml" (for the default SML engine) a
Am 12.06.2014 um 10:49 schrieb Gerwin Klein :
>> My suggestion would be not to add the new entries to "ROOT" (or wherever
>> they are listed), so that they are not tested at first.
>
> I’m very much against that:
>
> a) it would practically ensure they will never work. Nobody will notice, much
Am 12.06.2014 um 00:58 schrieb Gerwin Klein :
> In the first instance, it is the authors/maintainers of the entry that we
> will ask for help. In this case, Peter has promised to look at this set of
> new entries (CAVA etc), but it will take him some time.
>
> We usually have this state of affa
Hi all,
Albert Steckermeier (steckerm) has just been added to the Isabelle group. He's
a B.Sc. student who is working on an integration of the equality prover
Waldmeister with Sledgehammer. Like all my students, he will get the proper
repository training.
Jasmin
__
Hi Florian,
> many issues have been touched in this thread, but I would like to get
> back to the proposals made by Jasmin which IMHO point into the right
> direction.
Thanks for your comments. The current syntax (as per dc0b4f50e288) is
datatype_new (set: 'a) list (map: map rel: list_all2)
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson :
> What new users see when they look at the actual definition of lists is not
> that important. There are many, many situations where the actual definition
> of something is much more complicated than the idealised version that one
> would use fo
Am 26.05.2014 um 14:28 schrieb Andrei Popescu :
> I have the following proposal:
>
> (1) Hide all the extra structure from the user if it is not required
> explicitly.
>
> (2) Make parts of this structure visible upon request by "get" commands that
> specify the target datatype and the desired
> Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The constants
> from B are an integral part of the package---they form together with the type
> a BNF. Thus, they will always be "generated". The question is whether they
> are exposed to the user.
Well, they necessarily need to
Am 26.05.2014 um 10:30 schrieb Tobias Nipkow :
> I can only agree with what Makarius has observed but would go one step
> further:
> the new definition of list is truly baroque and unsuitable for beginners, but
> beginners are bound to look at it. Sometimes languages have to reduce
> complexity
Hi Makarius,
> For the new high-end BNF version of 'a list there were a few funny effects.
>
> (1) Its definition looks terrific:
>
> datatype_new (set: 'a) list (map: map rel: list_all2) =
>=: Nil (defaults tl: "[]") ("[]")
> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
>
> It means
> (For now the list of Remaining uses of Proof General / Emacs seems to be
> empty. If there is anything remaining, this thread is still open to
> submissions.)
Let me make this list nonempty again.
In the course of a day, I typically find myself pulling from the Isabelle
repository several t
Am 15.05.2014 um 18:59 schrieb Tobias Nipkow :
> Very good question. This is and has been the situation for a week or so:
>
> [Tycon] is still on FAIL.
> [Nominal2] is still on FAIL.
> [Incompleteness] is still on FAIL.
> [HyperCTL] is still on FAIL.
> [Launchbury] is still on FAIL.
>
> Could th
Hi René,
> I just wanted to report some unexpected behavior when adapting our theories
> to datatype_new.
> First of all, thanks for the development, the convenience of using this
> package is very welcome!
> (automatic generation of named selection, map, ..., speed, etc.).
> However, when playi
Am 13.05.2014 um 14:11 schrieb Manuel Eberl :
> In particular, any algebraic datatype with only one constructor can be
> rewritten into a corresponding codatatype, allowing you to use primcorec for
> it.
In fact, even (nonrecursive) datatypes with several constructors can be
rewritten into a c
Am 12.05.2014 um 23:10 schrieb Makarius :
> This sounds both a bit like "testing-unstable-HOL". But there is no problem
> to experiment with axiomatizations, if it clear to the user what it is, and
> not a seamingly harmless "bnf_decl".
For the record: The name "bnf_decl" was modeled after "ty
Hi Makarius,
Am 08.05.2014 um 12:32 schrieb Makarius :
> On Thu, 8 May 2014, mta-proj wrote:
>
>> die Gruppe isabelle, in der Sie Mitglied sind, wurde mit desharna,fleury
>> erweitert
>
> Membership of the "isabelle" Unix group means full root access to many
> administrative resources. Usual
Am 05.05.2014 um 11:17 schrieb Johannes Hölzl :
> Has anybody an idea why the AFP test for Probabilistic_Noninterference
> fails?
>
> When I build it on my machine
Same on my machine, and same for Selection_Heap_Sort, Native_Word, and
Launchbury: All work fine on my machine.
(HyperCTL has been
Hi all,
For the last three hours or so, the AFP Mercurial repository has been
unresponsive for me, "hanging" after:
$ hg out
comparing with ssh://blanche...@hg.code.sf.net/p/afp/code
or any other "hg" command requiring the server. :S
Jasmin
Hi all,
My work on (co)datatypes and my desire to move "Quickcheck_Narrowing" out of
HOL and into Library have lead me to discover several issues with the
interpretation mechanism ("Pure/interpretation.ML") that is used to hook into
various modules (e.g., the "size"-generating extension to "dat
I would like to add a fourth remark, mostly for the record:
>> macpro ad6bd8030d88
>> $ isabelle build -c -D Datatype_Test
>> Finished Datatype_Test_Old (0:14:31 elapsed time, 0:27:18 cpu time, factor
>> 1.88)
>> Finished Datatype_Test_New (0:05:11 elapsed time, 0:10:47 cpu time, factor
>> 2.08)
Hi all,
> So far the development has taken place in a private repository. I will move
> it to Isabelle next week (in "src/HOL/Tools/SMT2", in session "HOL-SMT2"). To
> be able to connect it with Sledgehammer's Isar proof generator, the best
> would be to make it part of the "HOL" session, but t
Hi Makarius,
Am 12.03.2014 um 13:33 schrieb Makarius :
> In Isabelle/4d46d53566e6 I've now made the innermost
> Proof_Context.transfer_syntax more efficient, by switching to a locally
> linear change discipline of the background theory that makes the merges with
> the corresponding tables with
Hi all,
As you may know, Sascha and I have been working on a new version of the "smt"
proof method, called "smt2". It is effectively a clone of "smt", but with the
Z3 interaction (problem generation, proof parsing, and reconstruction)
rewritten from scratch, with the following short-term goals:
Am 26.02.2014 um 19:26 schrieb Makarius :
> In the past few days AFP has been continuously broken: presently
> AFP/3fc9e6ace21f and Isabelle/1f27d75ccf05. After some time in a bad state it
> becomes increasingly difficult to guess which changes are responsible.
> http://isabelle.in.tum.de/repor
Am 21.02.2014 um 20:13 schrieb Florian Haftmann
:
>> *** Prover failed: error submitting job
>> *** At command "by" (line 28 of
>> "~~/src/HOL/Library/Sum_of_Squares_Remote.thy")
>> Unfinished session(s): HOL-Library
>> 0:07:48 elapsed time, 0:19:43 cpu time, factor 2.52
>
> Three weeks ago a r
Hi Josh,
Am 21.02.2014 um 07:12 schrieb Josh Tilles :
> Sure! There are some mathematical topics that I’d like to use Isabelle to
> study, but those topics require an intuitionistic setting. (the primary
> example is infinitesimal analysis) Also, the way that
> `src/HOL/ex/Higher_Order_Logic.t
Hi Josh, Lars,
Am 18.02.2014 um 08:19 schrieb Lars Noschinski :
> The position of the error message is a bit misleading. It is not the qed
> which fails. Instead, after finishing the proof, the free_constructors
> command tries to prove something on its own -- and fails. Probably, its
> intern
Am 12.02.2014 um 16:03 schrieb Makarius :
> I see a lot of incoming changes (and many hg queue accidents) just before
> that,
The "accidents" were that I experimented with "qfold" for the first time. The
command merges two patches together. The patches themselves were all as I
intended them to
Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel :
> Should be fine again (or at least better) with b445c39cc7e9. Thanks for the
> notification.
For the record: The goal state before and after had different variable names in
it. These become Skolem constants to Metis (in the FO logic sense, not i
Am 04.02.2014 um 10:25 schrieb Lars Noschinski :
> On 04.02.2014 01:05, Josh Tilles wrote:
>> Essentially, how do you configure Isabelle/jEdit when you want to make
>> changes to the "core" logics? (e.g., HOL, or even Pure)
>
> I don't think you can interactively make changes to Pure -- the proto
Hi all,
The "meson" proof method outputs some annoying messages like
0 inferences so far. Searching to depth 0
3 inferences so far. Searching to depth 5
6 inferences so far. Searching to depth 15
9 inferences so far. Searching to depth 25
12 inferences so far. Searching to depth 35
*** HOL ***
* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
"primrec_new", "primcorec", and "primcorecursive" command are now part of
"Main".
INCOMPATIBILITY.
Theory renamings:
FunDef.th
Hi Thomas,
Am 14.01.2014 um 14:43 schrieb Thomas Sewell :
> To address Jasmin and Larry's concern, it is possible to switch back to the
> "compatibility mode" by setting a config variable in the context, or by
> calling the ML version with an extra parameter. Any legacy proof script can
> be r
Hi Thomas,
Am 13.01.2014 um 13:38 schrieb Thomas Sewell :
> The change requires, for instance, about a dozen lines of changes to the
> files in HOL/Library, which contain about 50K lines of proof, or 3 lines of
> changes to HOL/Bali, with 30K. The change to the Nominal examples (30K),
> howeve
Am 07.01.2014 um 21:28 schrieb boeh...@in.tum.de:
> Unless Sledgehammer requires the remote_z3 service, any references to this
> obsolete service can now be removed from the code.
For users of two-core machines, the remote Z3 service might be of some use. But
this was much more relevant back in
Hi Florian,
Am 27.12.2013 um 10:04 schrieb Florian Haftmann
:
> But I am uncertain whether this timeout should be restricted to
> interactive mode anyway.
>
> Any suggestions?
I would suggest simply raising the timeout for that example. In
"Nitpick_Examples", we have had hard-coded timeouts f
Hi all,
The AFP tests are finally back, and this revealed a series of failures related
to my refactorings last week. Looking more closely at the falures, I found they
were all in the LaTeX generation, which I hadn't tested locally before pushing.
In most of the theories, it's the LaTeX symbol \
Hi all,
Back in August, I advertised our plan with the Bounded Natural Functor (BNF)
package. One of the items on the plan was to move the "datatype_new" command
into Isabelle before the Isabelle2013-1 release. After some reflection,
Makarius, Dmitriy, and I decided to postpone it to after the rel
Hi Florian,
My bad again. Fixed (578371ba74cc). Now I see why "pervasive = true" makes
sense.
Thanks for the notice.
BTW is there any particular reason why testboard and tests are kind of dead
these days?
Jasmin
Am 06.11.2013 um 21:12 schrieb Florian Haftmann
:
> isabelle b01057e72233 /
Sorry, fixed (81ee85f56e2d).
Jasmin
Am 01.11.2013 um 21:06 schrieb Florian Haftmann
:
> This refers to Isabelle hg id b1d955791529
>
>> Running HOL-Proofs-Extraction ...
>>
>> HOL-Predicate_Compile_Examples FAILED
>> (see also
>> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86
Am 03.10.2013 um 12:08 schrieb Tobias Nipkow :
> With Isabelle/jedit (566b769c3477) I get
>
> "remote_vampire": Error: SystemOnTPTP is currently not available: ERROR:
> Cannot
> make temp dir /tmp/SystemOnTPTPFormReply634.
>
> "remote_e_sine": Error: SystemOnTPTP is currently not available: ERR
Am 30.09.2013 um 15:07 schrieb Christian Sternagel :
> It seems that the required changes are minimal. See the attached patch. To be
> on the safe side: could somebody push this to the test server (in my local
> tests I just loaded all theories from the Isabelle repo and the AFP that
> containe
Am 27.09.2013 um 12:29 schrieb Peter Lammich :
> So here is my question:
> If I have some changeset, and want to check whether it breaks AFP
> before pushing it to the isabelle repository, how do I do it? Can I use
> Testboard?
I don't know if you're using queues, but what I typically do in such
Hi all,
Isabelle/jEdit is currently unwilling to process theories (as of dcefe11f28f2).
I open up an existing theory file, e.g.
isabelle jedit -l HOL-BNF src/Doc/Datatypes/Datatypes.thy
The file is correctly opened, but nothing is processed -- no imports are
processed, the theory text has
Am 24.09.2013 um 23:43 schrieb Makarius :
> This is a question to hard-core users of Mac OS X.
>
> How important is the canonical key sequence "COMMAND comma" as defined by
> Apple?
It's probably important, but I don't use it (for lack of having memorized it).
> Alternatively, I am open to sug
>> The first release candidates of Isabelle2013-1 will probably happen in the
>> first or second week of October.
>
> How is the general situation? And especially the situation for HOL-BNF?
"HOL-BNF" is a long-term construction yard. There happens to be a lot of
development these days, but it'
Dear all,
Starting with Isabelle/58d1b63bea81, Sledgehammer and Nitpick have a "spy" mode
[*] that log all invocations to those two tools in
"~/.isabelle/spy_{sledgehammer,nitpick}". If you are willing to be part of a
big experience in the name of science, please add
SLEDGEHAMMER_SPY=yes
Dear all,
I have moved to jEdit about one month ago. One bug that pops up now and then is
that some letters are not displayed (on Mac OS 10.8). This has happened
irregularly over the entire month. The screenshot below as taken against
d4a4b32038eb:
http://www21.in.tum.de/~blanchet/missing_
Hi Larry,
Am 12.09.2013 um 20:14 schrieb Lawrence Paulson :
> Provers don't launch at all (according to process monitor) and no output,
> either in the new S/H panel or via the sledgehammer command. I'm using
> 9d8764624487 but I don't think the precise version matters, as I grabbed a
> new co
Dear all,
As you might know, Andrei Popescu, Dmitriy Traytel, and I have been working on a
new (co)datatype package. It is part of Isabelle2013 in the directory
"src/HOL/Tools/BNF" (BNF = bounded natural functors) [1]. The package is
described in some detail in our LICS 2012 paper [2].
The packag
Hi all,
Using Isabelle/c3f837d92537,
theory Bug imports Main begin
lemma "(case p of (a, b) => f (a, b)) = f p"
raises
*** exception TERM raised (line 332 of "term.ML"): fastype_of: expected
function type
in Proof General and in "isabelle tty" but not in jEdit.
Needless to say,
Am 23.05.2013 um 14:30 schrieb Jasmin Christian Blanchette
:
> With the latest repository version (510709f8881d), I can't manage to build
> anything; e.g.
> […]
> I can't remember having done anything strange with my system except pulling
> some changes from the ma
Hi all,
With the latest repository version (510709f8881d), I can't manage to build
anything; e.g.
$ ./bin/isabelle build -c Pure
Running Pure ...
java.lang.NoSuchMethodError:
scala.Symbol$.apply(Ljava/lang/String;)Lscala/Symbol;
0:00:03 elapsed time, 0:00:04 cpu time
$ ./bi
Am 15.02.2013 um 13:37 schrieb Tobias Nipkow :
> Triggering s/h via "sorry" (or some other explicit means) is perfectly
> reasonable, but having the IDE invoke s/h based on time outs and guesses
> should
> be avoided: the success rate is low and it consumes a lot of resources.
>
> This is in con
Hi Tjark,
Am 11.02.2013 um 12:31 schrieb Tjark Weber:
> This continues to be a very minor issue, but perhaps it's still useful
> if I share my findings. The good news first: there already is an
> attribute to drop the name hint, namely
>
> ...[untagged "name"]
>
> Now the bad news: just like y
Hi Tjark,
Am 20.01.2013 um 22:21 schrieb Tjark Weber:
> On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
>> What's your concrete suggestion here?
>
> It's more of a curiosity than an issue, of course. Otherwise, I would
> suggest to: First, ma
Hi Tjark,
Am 18.01.2013 um 16:44 schrieb Tjark Weber:
> The new AFP entry on Kleene Algebras contains a metis call
> (http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652)
> that generates a warning about an unused theorem local.opp_mult_def.
>
Hi Makarius,
> http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Jan-2013/ is an early
> snapshot for the coming release. It is mainly a test of Isabelle packaging
> technology (not web technology). Components are taken from the
> Admin/components/ space within the repository.
It's nice to hav
Am 10.01.2013 um 13:16 schrieb Jasmin Blanchette:
> I just updated Isabelle to af8ecf09a58c (from a version that was one or two
> days old) and whenever I try to build HOL, I get this error:
>
>isabelle build -c -b HOL
>Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder gelade
Hi Gottfried,
Am 04.01.2013 um 14:09 schrieb Gottfried Barrow:
> So far I've managed to stay out of the development list, but this ties into
> what I saw in the past in my experiments with Sledgehammer, and how many ATPs
> it would launch at a time, which was a maximum of four even though an i7
Am 20.12.2012 um 21:30 schrieb Alexander Krauss:
> On 12/20/2012 12:20 AM, Alexander Krauss wrote:
>
>> (2) The local sysadmins are working on replacement of the Mercurial
>> 2.4 from SuSE 12.2, which is potentially the cause problems here.
>
> Replacement with what? Going to an older version is
Hi all,
The new "isabelle build" tool is really a joy to work with -- thanks Makarius!
:-) But one of the mistakes I find myself doing over and over is typing
isabelle build HOL
when I really meant
isabelle build -b HOL
Sometimes I don't even notice my mistake and find myself using an
Am 12.12.2012 um 19:29 schrieb Makarius:
> Are there actually Isabelle / Proof General 4.2 users around?
I think Larry gave it a try.
> For the coming Isabelle release, I need some hint if there will be a version
> of Proof General shipped with it at all, and which version it should be. If
>
Hi Sascha,
> Before Tobias' change, one sub-conversion (a rewr_conv) in that process
> returns a beta-reduced equation (reducing one of the above lambda
> abstractions), and hence the left-hand side does not match anymore the term
> given to the conversion.
Right now I am experiencing lots of
Hi all,
I'm trying to push changes to the Isabelle repository and got the following
error:
Übertrage nach
ssh://macbroy21.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
Suche nach Änderungen
Entfernt: Abbruch: Kann Projektarchiv
/home/isabelle-repository/repos/i
Am 05.12.2012 um 16:33 schrieb Tobias Nipkow:
> I tried again (but after some hg fetches, and am now on 3ae4376cb739), and now
> HOL still builds but HOLCF hangs. On the other hand Johannes (running Linux
> rather than MacOS) is fine. Suspicion: I had to do isabelle components -a this
> morning, a
Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:
> The real issue, at the end of the day, seems to be not so much Z3 4.0 in
> itself but rather the fact that our code often can't parse them. I've looked
> into this and saw no quick fix [*].
Oh, Tobias just remind
Hi Makarius,
Sascha and I are responsible for SMT. Sascha still occasionally works on it,
but I bear the ultimate responsibility for it now.
> Then running some examples with the current z3-4.0 version produced a lot of
> errors, see the included change for SMT_Examples.thy and the resulting
>
Am 03.12.2012 um 22:31 schrieb Jasmin Christian Blanchette:
> I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
> (40ecbad14077).
>
> 1. In Proof General:
>
>theory Scratch
>imports
> "$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
Hi all,
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
"$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe"
"~~/src/HOL/Proofs/Lambda/StrongNorm"
begin
nondeterministically gives either
*** Unde
Am 03.12.2012 um 11:02 schrieb Makarius:
> For Z3 in particular, there is also the problem that you have to be a
> non-commercial user to run it. This is hypothetical at the moment, since
> there are no commercial Isabelle or AFP maintainers.
Incidentally, for AFP, Tobias's policy is that "sm
Am 08.11.2012 um 12:56 schrieb Lawrence Paulson:
> The long-term solution must be to deliver self-contained proof scripts, but
> obviously it will be difficult.
Indeed. The good news is that the DFG accepted Tobias's project proposal called
"Hardening the Hammer", where the first item is about
Am 08.11.2012 um 11:55 schrieb Jasmin Christian Blanchette:
> I'll regenerate them [the certificates].
Actually, Z3 fails to refind the proof on my machine. Perhaps I'm using a
different version of Z3 than Ondrej used. So I've now delegated the issue to
Ondrej, who's mo
Hi Gerwin,
Am 07.11.2012 um 22:41 schrieb Gerwin Klein:
> *** Bad certificate cache: missing certificate
> *** At command "by" (line 169 of
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/AVL-Trees/AVL.thy")
> (real error)
OK, this is related to my Isabelle change 34b0464d7eef, which slightly affec
Hi all,
This is probably a question to Makarius. Today the Isatest reports look like
this:
Test for platform mac-poly64-M2 failed. Log file attached.
[...]
Finished at Wed Oct 24 02:40:50 CEST 2012
2:12:57 elapsed time, 3:44:19 cpu time, factor 1.68
--- test F
Am 16.10.2012 um 18:12 schrieb Lukas Bulwahn:
> NB: At the current tip d7917ec16288, I cannot find any duplicate theorem for
> Pair_inject.
prod.inject[THEN iffD1, THEN conjE]
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://ma
Hi Tjark,
Am 16.10.2012 um 13:22 schrieb Tjark Weber:
> Class semiring in HOL/Rings.thy [1] assumes
>
> left_distrib: "(a + b) * c = a * c + b * c"
> right_distrib: "a * (b + c) = a * b + a * c"
>
> This is different from the terminology used in Wikipedia [2],
> MathWorld [3] and much of the
Am 09.10.2012 um 16:27 schrieb Lawrence Paulson:
> I haven't studied the conditions in detail, but apparently the new licence
> for Z3 allows redistribution. And I imagine that allows it to be distributed
> as Isabelle component of sledgehammer.
We already had the explicit permission from the d
1 - 100 of 170 matches
Mail list logo
