Hi Florian,
Am 18.08.2011 um 09:18 schrieb Florian Haftmann:
@list: btw. what is the status of »refute« in general? Is it supposed
to be superseded by nitpick entirely?
Pretty much so, yes, but there are a few reasons why I would rather that we
keep it around:
1. Refute participates at
On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
[...] So, the best way now is
to continue eliminating set-pred mixture (also in the AFP of course!)
and discover problems in packages – I'm a little concerned about
quotient since this has
Hi all,
Let me describe the implications of reintroducing 'a set for Sledgehammer's
and Nitpick's performance.
Am 12.08.2011 um 11:27 schrieb Alexander Krauss:
What are, actually, the losses when going back? This has not yet been touched
by this thread at all (except the
On Thu, 18 Aug 2011, Florian Haftmann wrote:
envisaged working plan
--
a) general
b) elimination of set/pred mixture
c) consolidation
d) RELEASE
This looks quite reasonable to me: the parts a, b, c should be easy to
consolidate for the release towards the end of the
On 08/18/2011 02:16 PM, Florian Haftmann wrote:
* (maybe)
hide_fact (open) Set.mem_def Set.Collect_def
to indicate that something is going on with these
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs
that we know are going to break one release later...?
On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote:
The maintenance load is extremely low. When it comes to the REFUTE
exception, I can look at it if and when we decide to move back to
sets.
I suspect that Jasmin will have no trouble fixing this, but otherwise
I'd be happy to
Hi all,
Here are some critical questions/comments towards two of Florian's
initial arguments pro 'a set.
[...]
* Similarly, there is a vast proof search space for automated tools
which is not worth exploring since it leads to the »wrong world«, making
vain proof attempts lasting longer
Alexander Krauss wrote:
In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state) * (expr * state))
set,
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that are often specified in
terms of functions (finite maps, almost constant maps, etc.). Thus,
Tobias Nipkow wrote:
Am 12/08/2011 11:27, schrieb Alexander Krauss:
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any more pain, apart from what Florian already mentioned?
Am 19.08.2011 um 00:00 schrieb Stefan Berghofer:
thanks for your excellent report, I fully agree with this view. There is
often a tradeoff between executability and conciseness / abstractness of
specifications, so I don't think it is a good idea to tweak the logic in
such a way that it is
Florian Haftmann wrote:
just do something like (unfold mem_def) and your proof will be a mess
since you have switched to the wrong world.
Like any definition of a primitive operator, mem_def is not really intended
to be unfolded by the user, so don't be surprised if your proof is a mess
after
On 19/08/2011, at 5:56 AM, Alexander Krauss wrote:
Here are some critical questions/comments towards two of Florian's initial
arguments pro 'a set.
[...]
* Similarly, there is a vast proof search space for automated tools
which is not worth exploring since it leads to the »wrong world«,
On 19/08/2011, at 8:10 AM, Stefan Berghofer wrote:
Tobias Nipkow wrote:
Am 12/08/2011 11:27, schrieb Alexander Krauss:
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any
Am 19/08/2011 00:10, schrieb Stefan Berghofer:
Tobias Nipkow wrote:
Am 12/08/2011 11:27, schrieb Alexander Krauss:
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any more
Am 19/08/2011 00:00, schrieb Stefan Berghofer:
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that are often specified in
terms of functions
16 matches
Mail list logo
