XSB support is not available. Option xsb is ignored

[Bruce Matichuk]

I have XSB installed in /opt/local/lib

When I run idp (most recent version of 3.3.1)

I get a warning

Warning: XSB support is not available. Option xsb is ignored.

This happens when I run Iterated-induction.idp

I'm not sure but this might be the reason that the model doesn't work. I get an error

----> Something is wrong with our theory
Warning: The input contains aggregates. Non-cardinality aggregates will be dropped, resulting in a weaker form of entailment.
defined_functor '1' encountered near line 15 - treated as normal one!
(translated to '1')
defined_functor '2' encountered near line 16 - treated as normal one!
(translated to '2')
Warning: Could not prove invariant, but could not disprove it either
----> Prover could not prove the invariant
----> This is a model of T such that goal is reached
nil

[Ingmar Dasseville]

We can only support XSB when IDP is built with XSB from the start. If you really need XSB, then I suggest you build IDP yourself as we are unable to provide binaries with XSB at the moments.

I suspect the prover failure is independent and is caused by the lack of a proper SPASS installation. You can set the prover command by setting the stdoptions.provercommand variable. It's default is "SPASS -TPTP %i > %o"

[Bruce Matichuk]

I love IDP and would really like to use it in my research. But I'm having trouble with a few things.

The iterative-induction problem provided in the public sample set doesn't work and there is no way to figure out how to fix this problem.

I don't know enough about XSB or IDP to know whether or not this is required. I would be interested in learning more, however, none of the current IDP documentation (that I have found) says anything about XSB, how to use it, or in which contexts it would be valuable. My only concern is that I get a specific error message when I run the provided IDP binary that XSB cannot be used.

I don't know anything about SPASS and I can't see how the model accesses it - there is nothing explicit in the model. so unless it is automagically linked and used, I don't see how it would apply. If it is automagically linked, and it is causing a problem in this case, then there should be some instructions about how to make use of it AND the provided example problem should be updated appropriately.

I would be interested in building the app, but the download from the web site does not include build source (I'm not sure why there are build instructions because there is no code to build.)

[Joachim Jansen]

Hi Bruce,

it's great to see your interest regarding IDP. IDP is a research tool and as you've noticed, there are some rough edges in some of the features. Please bear with us on these :-)

With regards to SPASS - this is an external system (a theorem prover) that is used for some functionality in IDP: the example you've mentioned uses this in the isinvariant(T,invariant) call on line 156. Unless you're interested in proving invariants (without using a structure as reference), this shouldn't bother you.

XSB is also another system which we use to optimize some of the functionality needed when doing model expansion. This is no extra functionality and only results in a (albeit significant) speedup. If you're not comfortable compilling IDP yourself, you can try to use IDP's precompiled binaries, but never set stdoptions.xsb=true.

However, I definitely recommend compiling IDP yourself if you wish to use it to its fullest. We're preparing a source package download for the latest IDP version, so it should be up on sourceforge.net soon. If you wish to compile IDP, you'll have to do this in Linux as well. If you have any problems compiling IDP, please let us know!

Kindest regards,

Joachim

[Ingmar Dasseville]

I put the source of the new version online at https://sourceforge.net/projects/idp/files/idp-3.3.1-Source.tar.gz/download

Don't hesitate to contact us if we can be of further assistance.

[Bart Bogaerts]

Seems resolved