fact++ package under ubuntu

[cmaeder]

Hets uses fact++ version 1.6.1. The dynamic libraries needed by hets are supplied by the package libfactplusplusjni that is part of our own fact++ package. On utopic our fact++ package could be installed using the exact version by sudo apt-get install fact++=1.6.1-0ubuntu7

Ubuntu's newer version (1.6.2) does not supply libfactplusplusjni! The actual binary FaCT++ is not used by hets. So the right dependency is best installed by sudo apt-get install libfactplusplusjni. This dependency should be re-added to hets-ontology.

The actual problem is, that hets reports Fact as available prover without checking the dynamic library (/lib/libFaCTPlusPlusJNI.so) supplied by libfactplusplusjni.

[cmaeder]

Maybe the dependency libfactplusplusjni should be added to hets-core (and hets-server-core).

[tillmo]

Maybe the dependency libfactplusplusjni should be added to hets-core (and hets-server-core).

Yes please!

[jelmd]

Perhaps as recommended because it does not really depend on it?

[cmaeder]

It really depends, as it can be called and will crash. The alternative is to make hets smarter to recognize that it cannot run fact.

[tillmo]

So for now, it should depend on it. Later on, we may switch this to recommended.

[jelmd]

Ah ok. But wait, AFAICS hets already ships its own version below hets/hets-owl-tools/lib/{uk.ac.manchester.cs.owl.factplusplus-P5.0-v1.6.3.1.jar,/native/*/}

[cmaeder]

Yes, libfactplusplusjni additionally supplies native dynamic libraries that are needed, too.

[cmaeder]

Well, maybe the proper file from https://github.com/spechub/Hets/tree/master/OWL2/java/lib/native can be copied to the correct location by the hets installation itself. Currently this is separated.

[jelmd]

Ehmm, basically the JNI lib of fact++ is the same as the binary FaCT++, but without the main method and with the dyn lib/loadable JNI compat, interface, so that java app is able to call it. So if hets doesn't use it by itself, I think, just the proper environment variable needs to be set or param given to the jvm invokation, to pick it up automagically.

[cmaeder]

Currently, hets calls OWLFact.jar and OWLFactProver.jar that are created from the java sources under https://github.com/spechub/Hets/tree/master/OWL2/java/de/unibremen/informatik

If you can make these .jars use the FaCT++ binary instead of the JNI libs go ahead.

[jelmd]

Ehm, what I mean is: hets just needs to make sure, that the env var LD_LIBRARY_PATH_64 and LD_LIBRARY_PATH_32 contains the path (or if none of them is set LD_LIBRARY_PATH), where the jni lib lives and gets exported, i.e. passed in the env vector of the fork/exec call. If hets doesn't tweak anything when it execs some external things, it think, it should be even sufficient to set the related var, when hets gets started and it will find it.

Just checked: src/FaCT++.Java/uk/ac/manchester/cs/factplusplus/FaCTPlusPlus.java just calls System.loadLibrary("FaCTPlusPlusJNI") => Runtime.loadLibrary("FaCTPlusPlusJNI"), which looks up the lib in the standard places - see Runtime.html#loadLibrary

[cmaeder]

In https://github.com/spechub/Hets/blob/master/OWL2/ProveFact.hs (line 161-174) the file "libFaCTPlusPlusJNI.so" is actually searched. The proper position can be given via the HETS_JNI_LIBS environment variable.

[cmaeder]

Yet, the (architecture dependent) file "libFaCTPlusPlusJNI.so" needs to be installed.

[jelmd]

Ah, cool, so no problem at all, to use, whatever JNI lib one wanna use, as long as HETS_JNI_LIBS gets used first.

[jelmd]

Just found, that macosx' uname -m returns 'x8664' as well (like 64bit linux). Therefore switching over to uname -suname -m would be a little bit better? BTW: Since hets* depends on owltools now, re-using its stack may solve some problems automagically?

E.g. hets could perhaps use jfact instead (IIUIC jfact is the successor of fact++ and has no JNI problems)?

[eugenk]

I'm currently trying to create an OS X package in order to get Fact++ running with Hets. The official FaCTpp-OSX-v1.6.1.zip only contains libFaCTPlusPlusJNI.jnilib files. Also, when I compile it myself (1.6.4 is the only successfully compiiling version), I only get the files libFaCTPlusPlusJNI.jnilib and libfact.jnilib.

What do I need to do with them to get Fact++ working in Hets?

[cmaeder]

Sorry, I've no idea and never tried this.

[jelmd]

You may have a look at https://github.com/spechub/Hets/blob/makefile_enhancements/Makefile#L837

Wrt. hets it is sufficient to just put them into $(BASEDIR)/lib/native/uname -m/.

[cmaeder]

hets expects .so and not .jnilib files.

[jelmd]

Ohh, I thought the JVM is looking up native libs with using the .jnilib suffix (at least this is, what https://developer.apple.com/library/mac/documentation/Java/Conceptual/Java14Development/05-CoreJavaAPIs/CoreJavaAPIs.html suggests). If hets does an additional check, this one needs probably to be fixed. Otherwise I think we get also the "namespace" collision problem described 26 days ago.

[eugenk]

Where does Hets determine whether or not Fact is available as a prover?

[cmaeder]

Not at all, fact is simply listed as always being available in OWL2.Logic_OWL2

[cmaeder]

In OWL2.ProveFact I see

factConsChecker = (mkConsChecker "Fact" topS consCheck)
  { ccUsable = checkOWLjar factJarS }

[eugenk]

That's interesting. Then please explain me the following output on OS X:

wget --header="Accept: text/plain" https://ontohub.org/dol-examples/CompetencyQuestion.dol
hets -I
> use CompetencyQuestion.dol
Analyzing file CompetencyQuestion.dol as library CompetencyQuestion
logic OWL
Analyzing spec CompetencyQuestion?my_ont
Analyzing spec CompetencyQuestion?CQ1
Analyzing spec CompetencyQuestion?Scenario
Analyzing spec CompetencyQuestion?CQ2
CompetencyQuestion> dg-all auto
CompetencyQuestion> dg basic Scenario
CompetencyQuestion_Scenario> prover Fact
Error:
No applicable prover with name "Fact" found

On Ubuntu, however, I get:

wget --header="Accept: text/plain" https://ontohub.org/dol-examples/CompetencyQuestion.dol
hets -I
> use CompetencyQuestion.dol
Analyzing file CompetencyQuestion.dol as library CompetencyQuestion
logic OWL
Analyzing spec CompetencyQuestion?my_ont
Analyzing spec CompetencyQuestion?CQ1
Analyzing spec CompetencyQuestion?Scenario
Analyzing spec CompetencyQuestion?CQ2
CompetencyQuestion> dg-all auto
CompetencyQuestion> dg basic Scenario
CompetencyQuestion_Scenario> prover Fact
Hint: Using comorphism `id_OWL.ELQLRL-ALC`

[cmaeder]

On a Mac you could try to set HETS_JNI_LIBS to your libFaCTPlusPlusJNI.jnilib file and hope that it is picked up by the -Djava.library.path= java argument.

[eugenk]

I already tried this. It doesn't work

[cmaeder]

There's also

  { proverUsable = checkOWLjar factProverJarS }

Have you set HETS_OWL_TOOLS (see Common.ProverTools) properly to find the jars?

[eugenk]

Yes, the HETS_OWL_TOOLS variable is set to the directory that contains OWL2Parser.jar, OWLFact.jar, OWLFactProver.jar and so on (OWL2/java/build/)

[cmaeder]

Could you try to debug if the jar is actually detected in Common.ProverTools.check4jarFileWithDefault?

  hasJar <- doesFileExist $ pPath </> jar
  return (hasJar, pPath)

[cmaeder]

I hope Mac's case-insensitivity does not matter.

[eugenk]

Now it has been found. There was a problem with HETS_OWL_TOOLS: It has been redefined by the wrapper script.

[eugenk]

However, now I get

hasJni = False
hasJniLib = False

in OWL2.ProveFact.runTimedFact and Fact is not called (just as expected)

[cmaeder]

HETS_JNI_LIBS needs to be the directory and jlibName needs to be changed in the source.

[cmaeder]

hasJni must become True

[eugenk]

Ah, alright. Now it is True. Shall I create a pull request such that Hets supports Fact++ 1.6.4 with the JNI libs (only)?

[cmaeder]

A PR should not harm for reviewing

[cmaeder]

A mere branch is maybe sufficient.

[eugenk]

I tried to keep the compatibility to the .so files in there with #1619.

[jelmd]

IMHO the whole thing (checking for a certain binary) is a bad kludge, because here hets makes improper use of assumed JVM implementation details and therefore should be removed. This, as seen, makes the whole thing error prone and more complex w/o any need. Since there is already a wrapper script around hets, this one should be used to set corresponding variables, and that's it - means keep it small and simple => robust ;-)

[eugenk]

Done with 90551cbc7fe198962ea6b72bf9e8aa9ce059f6ba in #1619; please review.

[jelmd]

Not really, I mean rm the whole lib checking incl. HETS_JNI_LIBS handling, because it is wrong, it still hardcodes checks for binaries. Instead the path to the corresponding libs ($HETS_JNI_LIBS) should be prepend or append to the LD_LIBRARYPATH[{32|64}] in the hets wrapper script. Than you get real flexibility ;-)

[eugenk]

Just to be clear: You suggest that we remove the checks for specific file names libFaCTPlusPlusJNI.so and libFaCTPlusPlusJNI.jnilib (I agree) and instead of using HETS_JNI_LIBS in the code, we add a path to the LD_LIBRARY_PATH in the wrapper script?

I don't know enough of the java environment, so I need to ask: Do we need to explicitly set the -Djava.library.path= to the LD_LIBRARY_PATH when starting the java application? I couldn't find any sources on this.

[jelmd]

1) Yes.

2) No. JVM first tries to find the libname_.os_specificsuffix first in the system pathes and if not found than in the user pathes. The 1st consists usually of the sun.boot.library.path (i.e. something like /usr/jdk/instances/jdk1.7.0/jre/lib/{amd64|i386}. The 2nd is the value of -Djava.library.path=, or if unset an OS specific default path, which includes the pathes of LD_LIBRARYPATH[{32|64}], if any (on apple prefix with DY). [Might be different on windows, but who cares ;-) ]

[tillmo]

maybe this can be solved by moving to a new version of Fact, see #1616

[jelmd]

BTW: IIRC the plan is to move to OWL API 4.x? And Fact++ supports OWL API 3.x, only? If so moving to jfact (supports OWL API 4.x) is needed anyway?

Because jfact is a pure java app, the JNI problem would go away automagically when switching over to it. One just needs to figure out, what the "Bremen layer" mentioned at the top of this thread really does. Just glue the haskell code with the native library? In this case perhaps the jfact API/CLI can be used directly to replace it?

[tillmo]

The plan to move to OWL API 4.x in #1891 is meant for Hets' parsing purposes only. Note that a prover needs to parse the OWL file again and typically calls its own instance of the OWL API (which can have a different version). So these are two different problems.

I do not know about jfact; its documentation seems to be nonexistent.

[jelmd]

Ah ok, so we keep it as is.

BTW: jfact: http://jfact.sourceforge.net/ - I guess there is no separate doc because "its design matches FaCT++ design very closely".