Email Gateway (Dec 22 2021 at 14:20): Email Gateway (Dec 22 2021 at 14:20):From: David Fuenmayor <davfuenmayor@gmail.com>
I would like to use Isabelle with the 'minimal' possible library imports
(and therefore not importing Main).
By 'minimal' I mean this: using Isabelle as a proof assistant for simple
type theory (+ choice, prefix polymorphism, etc.) in such a way that
Nitpick and the integration with external ATPs (via Sledgehammer + proof
reconstruction with metis, smt & co.) still work, and nothing more.
One motivation is (i) being able to invoke Sledgehammer with as few facts
as possible, without "polluting" invocations with facts from the libraries
(for which I have no use at present). Other motivation (ii) is improving
performance in general (also for Nitpick), e.g. when using Isabelle in
headless mode.
I know that for (i) one can manually select which facts are passed to
Sledgehammer (though I wouldn't like to always think about this). As for
(ii) I would like to know whether there are (or not) any differences.
Thanks for the help (and happy Christmas time!)
David
Email Gateway (Dec 23 2021 at 08:50):From: Fabian Huch <huch@in.tum.de>
On 12/22/21 15:19, David Fuenmayor wrote:
I would like to use Isabelle with the 'minimal' possible library
imports (and therefore not importing Main).
By 'minimal' I mean this: using Isabelle as a proof assistant for
simple type theory (+ choice, prefix polymorphism, etc.) in such a way
that Nitpick and the integration with external ATPs (via Sledgehammer
+ proof reconstruction with metis, smt & co.) still work, and nothing
more.
The minimal import of Isabelle is Pure. However, sledgehammer and
nitpick are implemented in HOL. You can import just those tools and
their dependencies; you don't need to use Main. But if you want to have
those tools in another object logic, you'll have to implement them there.
Other motivation (ii) is improving performance in general (also for
Nitpick), e.g. when using Isabelle in headless mode.
For that, build a minimal session which contains just the (closure of)
imports of those tools.
One motivation is (i) being able to invoke Sledgehammer with as few
facts as possible, without "polluting" invocations with facts from the
libraries (for which I have no use at present).
I know that for (i) one can manually select which facts are passed to
Sledgehammer (though I wouldn't like to always think about this).
You can easily achieve this by writing a sledgehammer' command which
excludes the facts that you don't want.
Fabian
Email Gateway (Dec 23 2021 at 10:48):From: Lawrence Paulson <lp15@cam.ac.uk>
I would be surprised if this minimal system delivered many benefits. On the other hand, it would be interesting to find out. I hope you will report back with some measurements in a couple of months.
Larry
Email Gateway (Dec 23 2021 at 11:06):From: Makarius <makarius@sketis.net>
On 22/12/2021 15:19, David Fuenmayor wrote:
I would like to use Isabelle with the 'minimal' possible library imports (and
therefore not importing Main).
This is not officially supported. The canonical entry points for Isabelle
applications are:
* Pure: minimal higher-order logic as a logical framework for object-logics,
or complete different applications based on ML and lambda-calculus.
* Main: full higher-order logic with "batteries included", i.e. many
fundamental concepts expected from logic and functional programming (this is
not yet "library").
* Complex_Main: add-ons to Main from classic mathematics (rat, real, complex).
Anything between Pure -- Main -- Complex_Main is an implementation detail, and
to be considered "private" (as in a Java or Scala library).
Only on top of HOL Main and Complex_Main we can speak of genuine libraries:
here you import the subgraphs that you require.
Sometimes such libraries are wrapped-up in a similar manner as Main, e.g.
HOL-Analysis.Analysis: It would be better if Isabelle would support an
official "private" marker to theories and libraries would use that.
One motivation is (i) being able to invoke Sledgehammer with as few facts as
possible, without "polluting" invocations with facts from the libraries (for
which I have no use at present). Other motivation (ii) is improving
performance in general (also for Nitpick), e.g. when using Isabelle in
headless mode.
Isabelle tools are normally constructed to work in large theory contexts,
because this is the normal situation. It is unlikely that a deconstruction of
works substantially better, just by stripping away things.
Anyway, what exactly do you mean by "performance ... in headless mode"? What
is the hardware behind that? Something like Raspberry Pi or a regular cloud
node (e.g. 2 CPU cores + 8 GB should be just fine for small applications)?
I know that for (i) one can manually select which facts are passed to
Sledgehammer (though I wouldn't like to always think about this). As for (ii)
I would like to know whether there are (or not) any differences.
Fact selection is a special topic for Sledgehammer. The makers of that great
tool can tell you what are potential approaches to improve on that.
Makarius
Email Gateway (Dec 24 2021 at 16:11):From: David Fuenmayor <davfuenmayor@gmail.com>
Thanks for the answers. I understand that there is little that can be done
for my case.
I found out that by importing only the theory "Nitpick" I can get to run
all of my current experiments (a formalization of basic topology).
In fact, I noticed that I don't even need to import theory "Sledgehammer",
which is a direct import of theory "List", since the latter ends up being a
transitive dependency of "Nitpick".
I must admit that I don't always understand the reasons behind these
dependencies. In any case, it seems that I just cannot use nitpick without
loading a lot of HOL libraries (sets, lists, numbers, etc) and
infrastructure (for codegen, lifting, etc,) for which I don't have any use
in my work.
@Fabian:
You can easily achieve this by writing a sledgehammer' command which
excludes the facts that you don't want.
Right. I think I will now manually put my facts in "named_theorems" and
pass exclusively the latter to sledgehammer.
@Makarius
Anyway, what exactly do you mean by "performance ... in headless mode"? What
is the hardware behind that? Something like Raspberry Pi or a regular cloud
node (e.g. 2 CPU cores + 8 GB should be just fine for small applications)?
I am working with container-based, pay-as-you-go (aka. "serverless")
computing infrastructure. For instance, in AWS Fargate you pay per used
vCPU and GB RAM (https://aws.amazon.com/fargate/pricing/), also in AWS
Lambda computing nodes start already with 128Mb RAM (
https://aws.amazon.com/lambda/pricing/). Other providers (azure, google.
etc.) have similar offerings. Cloud computing is forcing software engineers
to become stingy again!
Fact selection is a special topic for Sledgehammer. The makers of that great
tool can tell you what are potential approaches to improve on that.
I have to admit that mesh, mepo & co. do a great job! So I have been able
to mindlessly hammer my way through so far :)
Last updated: Jul 15 2022 at 23:21 UTC