Stream: General

Topic: Running Isabelle on Linux systems with musl-libc

view this post on Zulip Shuhan Hŏ (Aug 08 2024 at 02:31):

Hi all, the Isabelle2024 distribution for Linux does not run on my musl-libc based system. The bundled java complains "cannot execute: required file not found". Any solutions, please?

view this post on Zulip irvin (Oct 02 2024 at 20:56):

This is a bit late but afaik nix builds isabelle from scratch. You could look to see what nix does and try to build it fixing the dependency issues as you go along

view this post on Zulip Shuhan Hŏ (Oct 02 2024 at 23:31):

Thanks a lot for actually pointing me in the right direction! You have been so much more helpful than M Wenzel.

view this post on Zulip Jan van Brügge (Oct 03 2024 at 08:33):

Nix does not quite build isabelle from Scratch. All the components aside from polyml and java are just patched. However that might still be enough

view this post on Zulip Nges Brian (Oct 04 2024 at 22:59):

In the past few days, I have read a few papers on Autocorres and I am excited about the tool and I want to use it in building my own C applications. At this point, I want to try it out but I am new to both Isabelle and Autocorres.

From the information I have gathered, Autocorres is a package used in Isabelle and to set it up,
I have taken the following steps:

1) Downloaded the Autocorres 1.10 package from https://github.com/seL4/l4v/releases ( autocorres-1.10.tar.gz ) which works with Isabelle2023.

2) I download Isabelle2023 for my system which is Ubuntu22.04 (intel x86_64) from https://isabelle.in.tum.de/website-Isabelle2023/installation.html and install it following the instructions which is basically unzipping using the command

tar -xzf Isabelle2023_linux.tar.gz

3) I then install Autocorres using the following command

L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorres

4) Everything works as expected when I run the Autocorres Testsuites

L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorresTest

5) I have created a folder (~/Documents/fv) under which I have placed autocorres1.10 and Isabelle2023 folders. I have also created a folder test_programs which contain a c file minmax.c which contains the min and max functions written in c.

6) To formally verify this c functions, I open up Isabelle2023 GUI from my fv folder using the command

Isabelle2023/Isabelle2023

7) I create a new file in my test_programs called minmax.thy which contains the following Isabelle code

theory minmax
 imports AutoCorres
begin
  external_file "./minmax.c"
  install_C_file "./minmax.c"
  autocorres [ts_rules = nondet] "minmax.c"
end

when I run this, I get the error:

Bad theory import "Draft.AutoCorres"

I do not know what I am missing in the setup process and I will be glad if I can get some help in setting this things up and using Autocorres to verify C programs.

view this post on Zulip Shuhan Hŏ (Oct 05 2024 at 01:41):

I have been trying to bootstrap Isabelle/Pure from scratch, using src/Pure/ROOT.ML as a starting point; it seems possible to build a bare-bones Pure environment that relies on nothing but PolyML.

view this post on Zulip Yong Kiam (Oct 05 2024 at 02:09):

Nges Brian said:

In the past few days, I have read a few papers on Autocorres and I am excited about the tool and I want to use it in building my own C applications. At this point, I want to try it out but I am new to both Isabelle and Autocorres.

From the information I have gathered, Autocorres is a package used in Isabelle and to set it up,
I have taken the following steps:

1) Downloaded the Autocorres 1.10 package from https://github.com/seL4/l4v/releases ( autocorres-1.10.tar.gz ) which works with Isabelle2023.

2) I download Isabelle2023 for my system which is Ubuntu22.04 (intel x86_64) from https://isabelle.in.tum.de/website-Isabelle2023/installation.html and install it following the instructions which is basically unzipping using the command

tar -xzf Isabelle2023_linux.tar.gz

3) I then install Autocorres using the following command

L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorres

4) Everything works as expected when I run the Autocorres Testsuites

L4V_ARCH=X64 Isabelle2023/bin/isabelle build -d . AutoCorresTest

5) I have created a folder (~/Documents/fv) under which I have placed autocorres1.10 and Isabelle2023 folders. I have also created a folder test_programs which contain a c file minmax.c which contains the min and max functions written in c.

6) To formally verify this c functions, I open up Isabelle2023 GUI from my fv folder using the command

Isabelle2023/Isabelle2023

7) I create a new file in my test_programs called minmax.thy which contains the following Isabelle code

theory minmax
 imports AutoCorres
begin
  external_file "./minmax.c"
  install_C_file "./minmax.c"
  autocorres [ts_rules = nondet] "minmax.c"
end

when I run this, I get the error:

Bad theory import "Draft.AutoCorres"

I do not know what I am missing in the setup process and I will be glad if I can get some help in setting this things up and using Autocorres to verify C programs.

you may get better traction writing this as a separate thread in #Beginner Questions or similar

also, my understanding is that the latest AutoCorres is here:

https://www.isa-afp.org/entries/AutoCorres2.html

(although I have not used it myself)

view this post on Zulip irvin (Oct 05 2024 at 16:40):

Shuhan Hŏ said:

I have been trying to bootstrap Isabelle/Pure from scratch, using src/Pure/ROOT.ML as a starting point; it seems possible to build a bare-bones Pure environment that relies on nothing but PolyML.

The console using polyml is dead and everything is now using the Isar stuff which i dont think is supported by console.**
I have managed to get some process on getting it to run alpine linux

view this post on Zulip irvin (Oct 05 2024 at 16:45):

Documenting my steps now.

  1. download the repo version
  2. run Admin/init (warning the download is extremely slow and is done in serial) I have a patch that parallelizes it)
  3. Admin/init fails due to java. patch to use system java and then run Admin/init again
  4. Run isabelle jedit. Isabelle attempts to build HOL fails to build to some bash_process.
  5. Go to bash_process. build bash_process.c. run isabelle jedit again
  6. Poly fails patch to use system poly
  7. Poly now fails to a error Can't unify int (In Basis) with LargeInt.int (In Basis) (Different type constructors) (distribution polyml was built without using gmp for int.)
  8. Build poly isabelle component_jdk (use -v to debug if it fails)
  9. Patch isabelle to use the newly build components
  10. Pure succeeded in building
  11. Isabelle attempts to build HOL fails and crashes after build HOL.Equiv_Relations.
  12. Ok so launching isabelle using Pure (isabelle jedit -l Pure) it seems to be that its failing cuz of too little memory in vm. After upgrading it seems now that its failing whenever a proof use smt. Weird thought smt is discouraged. So next would be to build the sledgehammer provers

view this post on Zulip irvin (Oct 05 2024 at 18:32):

Current Status on musl: Isabelle works if you dont use smt tactic
isabelle can run with Pure just fine. Isabelle can run anything before HOL.Sledgehammer.
Things that work
Inductive
datatypes work.
try0 seems to work
function package
Things that dont work
HOL.List there is one call to smt there
Code numeral. So no nice syntax for numbers
codatatypes. they depend on HOL.list
record types.
quickcheck/nitpick

view this post on Zulip Mathias Fleury (Oct 05 2024 at 20:04):

The smt method requires you to recompile z3 and veriT. For veriT running isabelle component_verit might be sufficient

view this post on Zulip Mathias Fleury (Oct 05 2024 at 20:06):

(for cvc, vampire, E, spass, ziperposition: these are only used in sledgehammer)

view this post on Zulip irvin (Oct 06 2024 at 08:56):

Mathias Fleury said:

The smt method requires you to recompile z3 and veriT. For veriT running isabelle component_verit might be sufficient

Yup building verit managed to get HOL to build now building afp. I dont think afp is going to affect anything but just building for testing purposes

view this post on Zulip irvin (Oct 06 2024 at 09:14):

Side note is smt an oracle or proofterm is generated?

view this post on Zulip irvin (Oct 06 2024 at 10:51):

Ok some of afp fail. Some error msg unclear but z3 failures are quite clear

view this post on Zulip Mathias Fleury (Oct 06 2024 at 13:00):

irvin said:

Side note is smt an oracle or proofterm is generated?

unless you activate the smt_oracle (which you do not in AFP), the proofs by the smt solver is checked

view this post on Zulip Mathias Fleury (Oct 06 2024 at 13:03):

If you run an smt proof with supply [[smt_trace]] you will see the reasoning steps

view this post on Zulip irvin (Oct 07 2024 at 19:43):

Is there any reason other than a lack of resources that isabelle uses such an old version of z3.

view this post on Zulip irvin (Oct 07 2024 at 19:44):

Even gcc right now cant build z3. Need to use an older version.

view this post on Zulip irvin (Oct 07 2024 at 19:46):

Modern z3 /lastest version does seem to work (unknown method proof-term).
And slightly updated version which work for isabelle and build have the slight issue of causing some z3 calls to fail

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:51):

irvin said:

Is there any reason other than a lack of resources that isabelle uses such an old version of z3.

the proof format changed slightly in slightly newer z3 version

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:51):

which means that smt will fail in some cases

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:51):

and in even more recent version the generated proof are incorrect (I discovered that when I tried to update z3)

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:52):

see issue https://github.com/Z3Prover/z3/issues/5073

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:53):

So: there is a lack of resources to investigate how far you can update (I still hope to get a student to show up that wants to work on that, because I do not have the time to do it)

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:54):

And: updating z3 can break the AFP

view this post on Zulip Mathias Fleury (Oct 07 2024 at 19:54):

(actually it has not been tried)

view this post on Zulip irvin (Oct 07 2024 at 20:27):

Mathias Fleury said:

And: updating z3 can break the AFP

Yup that's what happened. building z3 git tag 4.5.0 can be done with modern gcc. But still some smt z3 calls fail. Anyway I probably stop trying to get isabelle to run on Alpine. Since it can be considered as usable.

view this post on Zulip irvin (Oct 07 2024 at 20:27):

Mathias Fleury said:

So: there is a lack of resources to investigate how far you can update (I still hope to get a student to show up that wants to work on that, because I do not have the time to do it)

Can i try to work on that?

view this post on Zulip Mathias Fleury (Oct 09 2024 at 05:00):

I have no idea who you are but: yeah sure

view this post on Zulip Mathias Fleury (Oct 09 2024 at 05:01):

but I guess you need a description on how to do that?

view this post on Zulip irvin (Oct 10 2024 at 00:44):

Mathias Fleury said:

but I guess you need a description on how to do that?

Yup. From most of my experience isabelle stuff is documented in papers. So i guess which papers document the smt method?

Last updated: Dec 21 2024 at 12:33 UTC