Stream: Isabelle/ML

Topic: Entry point for Sledgehammer’s external prover interface

view this post on Zulip Jiangjing Xu (Nov 27 2025 at 12:12):

Dear Isabelle developers,

I hope you are doing well. I am a student currently working on a university project regarding the reliability and testing of proof assistants. According to the project specification, my task is to test the interface between Isabelle/HOL and external provers, which are primarily invoked via Sledgehammer.

My supervisor recommended that I consult this community to better understand the internal architecture. In particular, I would be very grateful if you could advise me on the following:

  1. What is the main ML entry point or API through which Sledgehammer invokes external provers (such as E, Vampire, Z3)?

  2. Which modules or functions in the Isabelle code base are responsible for:
    (a) preparing problems for external provers
    (b) launching the external tools
    (c) parsing and integrating their results back into Isabelle?

  3. If one wishes to instrument or fuzz the interface (for example, by injecting mutated prover calls or modified problem files), is there a recommended way to call this layer programmatically?

For context, I am working with Isabelle 2025, and this question is specifically motivated by Variant 3 of my project, which focuses on exercising the Sledgehammer–external prover interaction to search for crashes, miscommunication, hangs, or unexpected behaviours.

Thank you very much for your time and guidance. I sincerely appreciate your help as I am still learning the internal structure of Isabelle.

Kind regards,
Jiangjing Xu

view this post on Zulip Fabian Huch (Nov 27 2025 at 12:36):

Have a look at the function Sledgehammer_Prover_ATP.run_atp (In the file src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML), where all of this happens.

This calls all the components, e.g. ATP_Problem_Generate.generate_atp_problem (in src/HOL/Tools/ATP/atp_problem_generate.ML).

You can simply write Isabelle/ML code to call the involved functions yourself.

view this post on Zulip Fabian Huch (Nov 27 2025 at 12:41):

If you're new to Isabelle/ML, have a look at the first few sections of the Isabelle/ML Cookbook.

view this post on Zulip Kevin Kappelmann (Nov 27 2025 at 12:43):

Fabian Huch said:

If you're new to Isabelle/ML, have a look at the first few sections of the Isabelle/ML Cookbook.

That's the 2013 version. Here's the most up-to-date version (2019): https://urbanchr.github.io/Cookbook/

view this post on Zulip Jiangjing Xu (Nov 27 2025 at 15:31):

Fabian Huch 发言道：

Have a look at the function Sledgehammer_Prover_ATP.run_atp (In the file src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML), where all of this happens.

This calls all the components, e.g. ATP_Problem_Generate.generate_atp_problem (in src/HOL/Tools/ATP/atp_problem_generate.ML).

You can simply write Isabelle/ML code to call the involved functions yourself.

Thank you very much, Mr.Huch — this is extremely helpful.

I will look into Sledgehammer_Prover_ATP.run_atp and the related modules you mentioned, especially ATP_Problem_Generate.generate_atp_problem. This gives me a clear starting point for understanding the full invocation chain.

I appreciate the guidance on calling these components directly from Isabelle/ML as well.

view this post on Zulip Jiangjing Xu (Nov 27 2025 at 15:33):

Kevin Kappelmann 发言道：

Fabian Huch said:

If you're new to Isabelle/ML, have a look at the first few sections of the Isabelle/ML Cookbook.

That's the 2013 version. Here's the most up-to-date version (2019): https://urbanchr.github.io/Cookbook/

Thank you, Mr.Kappelmann, for the link to the updated Isabelle/ML Cookbook. I really appreciate it — I will study the 2019 version to familiarise myself with Isabelle/ML before diving deeper into the Sledgehammer interface.

view this post on Zulip Mathias Fleury (Nov 27 2025 at 16:14):

It seems strange to me to try fuzzing E and Vampire this way, because Isabelle does not really try to reconstruct the proofs

view this post on Zulip Mathias Fleury (Nov 27 2025 at 16:14):

Fuzzing the smt code that seems like a lot of fun :-)

view this post on Zulip Mathias Fleury (Nov 27 2025 at 16:15):

But: I expect that will find a lot of proof reconstruction problems

view this post on Zulip Mathias Fleury (Nov 27 2025 at 16:16):

before finding problems due to mutation

view this post on Zulip Mathias Fleury (Nov 27 2025 at 16:17):

BTW, I have somewhere a check_smt method that parses an input and a proof file. That might be useful to start fuzzing (you can mutate text files, which is easier than attempting to mutate the file generation itself)

Last updated: Dec 07 2025 at 04:34 UTC