thahmann / macleod Goto Github PK

It would be great to see macleod released on PyPI

I would be happy to help with this if you don't have the bandwidth

Currently, we are using the method discussed in #9 for p_error. This method utilizes lookahead tokens to illustrate the current state of the parse.

Unfortunately, this method doesn't allow us to do any form of error recovery, as the parser has already "looked ahead" to the EOF. It seems like we can either have this stack reporting algorithm or some error recovery algorithm, but not both.

I personally lean towards trying to do error recovery, but I don't want to make changes without some agreement. Thoughts?

The following error gets thrown for some CLIF files with imports:

2020-03-25 23:30:54,626 macleod.Commands DEBUG CONSTRUCTING COMMAND FOR: prover9 FROM /Users/cchui/Documents/GitHub/colore/ontologies/kinship/kinship.clif 2020-03-25 23:30:54,626 bin.clif_converter INFO Converting /Users/cchui/Documents/GitHub/colore/ontologies/kinship/kinship.clif to ladr format Traceback (most recent call last): File "macleod/gui/gui_beta/gui_main.py", line 299, in check_consistency_command (return_value, fastest_reasoner) = ontology.check_consistency(resolve=True) File "/Users/cchui/Documents/GitHub/macleod/macleod/Ontology.py", line 217, in check_consistency reasoners.constructAllCommands(self) File "/Users/cchui/Documents/GitHub/macleod/macleod/ReasonerSet.py", line 38, in constructAllCommands r.constructCommand(ontology) File "/Users/cchui/Documents/GitHub/macleod/macleod/Reasoner.py", line 65, in constructCommand self.args = commands.get_system_command(self.name, ontology) File "/Users/cchui/Documents/GitHub/macleod/macleod/Commands.py", line 26, in get_system_command return handlers.get(system_name, get_empty_cmd)(ontology) File "/Users/cchui/Documents/GitHub/macleod/macleod/Commands.py", line 39, in get_p9_cmd args.append(clif_converter.convert_single_clif_file(ontology,clif_converter.ladr_output,True)) File "/Users/cchui/Documents/GitHub/macleod/bin/clif_converter.py", line 32, in convert_single_clif_file results = ontology.to_ladr(resolve) File "/Users/cchui/Documents/GitHub/macleod/macleod/Ontology.py", line 194, in to_ladr all_modules = self.get_all_modules() File "/Users/cchui/Documents/GitHub/macleod/macleod/Ontology.py", line 131, in get_all_modules print ("Found import " + onto.name) AttributeError: 'NoneType' object has no attribute 'name' Abort trap: 6
What happens:

• Python3 crashes
• GUI closes automatically

Test file:

• http://colore.oor.net/kinship/kinship.clif

I've checked the imports and the CLIF files themselves look fine and don't appear to have any syntax errors. It seems like the imported CLIF files don't get initialized with the 'name' attribute when it gets parsed by Macleod.

Any thoughts on what might be causing this?

The method

I may be incorrect about this, but Parser.py doesn't seem able to use the prefix setting from the conf file. It seems that almost all cl-imports in COLORE start with "http://colore.oor.net". Right now, Parser.py tries to read these URLs as paths.

At the moment we have three separate configuration files in the conf/ directory. The only difference between them are paths to base directories and command names/return values. It might be better to take the existing configuration files and place them under doc/sample_config for reference.

We would then update the software to look in the $USER/.macleod (*Nix) or $USER/macleod directory for a single configuration file. Setting the correct config values is then an installation step where a user copies the closest configuration and updates it accordingly.

This would also keep us from getting our config files stuck in the baseline every so often.

After synchronizing this commit @thahmanncaae8b5 , I came across this error in the OS X Terminal:
bad magic number in 'macleod': b'\x03\xf3\r\n': ImportError

It can be fixed by deleting the Python cache for the macleod directory:
find . -name \*.pyc -delete

Not sure if this is worth including in the README or the installation instructions if others come across this error while running macleod.

There are times where we need a list of all axioms found in a theory in one single CLIF file to make it easier to view all of the axioms in one place.

While the current macleod scripts do do this with the LADR and TPTP conversions, we would also be interested in having this in the CLIF format.

e.g., take http://colore.oor.net/fount/fount.clif for example -- this is a theory that imports a lot of theories.

Due to the sheer volume of imports, it is not manageable to do the imports manually (through copying and pasting), so it might be beneficial to have a script that can do this automatically when the imports are parsed in the macleod GUI.

Currently, main log file is located relative to path from where the scripts are executed (often in the ontologies folder), while the macleod_sub log file is located in the macleod\log directory.
Need to create a unified location and make sure the folder is created if it doesn't exist.

Hi Torsten,

I noticed you've made some changes to macleod -- I actually have a new MacBook and was trying to install the latest version of macleod on this new computer.

I came across this error message:

Traceback (most recent call last): File "gui_beta/gui_main.py", line 284, in <module> window = MacleodWindow() File "gui_beta/gui_main.py", line 40, in __init__ self.setup_widgets() File "gui_beta/gui_main.py", line 45, in setup_widgets self.editor_pane = gui_widgets.TabController(self, self.ontologies) File "/Users/cchui/Documents/GitHub/macleod/macleod/gui/gui_beta/gui_widgets.py", line 16, in __init__ self.add_file() File "/Users/cchui/Documents/GitHub/macleod/macleod/gui/gui_beta/gui_widgets.py", line 32, in add_file gui_highlighter.CLIFSyntaxHighlighter(new_tab, None, None) File "/Users/cchui/Documents/GitHub/macleod/macleod/gui/gui_beta/gui_highlighter.py", line 24, in __init__ self.format_predicate.setForeground(get_color("color_predicate")) File "/Users/cchui/Documents/GitHub/macleod/macleod/gui/gui_beta/gui_highlighter.py", line 93, in get_color return QColor(filemgt.read_config("gui", setting_name, filemgt.config_file)) AttributeError: module 'macleod.Filemgt' has no attribute 'config_file'

(Screenshot enclosed below.)

Does gui_beta work with the changes that you've made? Or should I try gui_alpha? I have both Python 2.7.10 and Python 3.7.2 installed on this new machine.

TPTP needs constants to be wrapped in either single quotes (') to represent constants or (") to represent disjoint constants.

Currently the FileMgmt.py does a lot of extra work to find its configuration files. To support the single defined-by-user-account configuration store the config_dir path is hardcoded to be userName/macleod/. From there the rest of the code is as-is and does a bunch of stuff to "locate" the files contained in that directory.

There is logic in there for the sub-process logs that I didn't want to touch. It could all be simplified since we now have fixed locations for the log files.

Currently the header style comment blocks that sometimes appear at the beginning of clif files cause the parser to fail if one is encountered mid file.

Refactor the clif.py [get_nonlogical_symbol_arity] function to eliminate the nested inner function [find_symbol_arity]

1. Replace with an interface clif.py [get_nonlogical_symbol_arity_from_file] that translates for a new [get_nonlogical_symbol_arity] function.
2. Separate file loading, validation, parsing, and extraction into different ClifModule (ClifFile?) states.

If I remember correctly it was working as intended but it should be tested to make sure. The only remaining issue was how to properly copy/place the configuration files in a users home directory. M

Hello,

Thanks for the great tool. I am still trying to get familiar with it and I was wondering if there is a particular reason that the config is always searched in the specific user folder.

I think it would be great to have configs that are project specific. Namely, let the Filemgt search first in the current directory for a config would be very practical. That way is easier to organise different ontology projects independently.

If I get the time to get into it and I understand the tool enough I will do a PR. Unless you are preparing something already

It seems like some axioms are not fully splitted into separate FF-PCNF conjunction, for example:

Axiom: \forall x,y;[(~((AB(x) | PD(x)) & ~P(x,y)) | \exists z;[(P(z,x) & ~O(z,y))])] from http://colore.oor.net/dolce_mereology/dolce_mereology.clif
FF-PCNF: \forall z,y;[\exists x;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]]

• yielded: \forall z,y;[\exists x;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]]

I believe
FF-PCNF: \forall z,y;[\exists x;[((~AB(z) | P(z,y) | P(x,z)) & (~AB(z) | P(z,y) | ~O(x,y)) & (~PD(z) | P(z,y) | P(x,z)) & (~PD(z) | P(z,y) | ~O(x,y)))]]
should be split into four separate PCNF sentences:
\forall z,y;[\exists x;[(~AB(z) | P(z,y) | P(x,z))]]
\forall z,y;[\exists x;[(~AB(z) | P(z,y) | ~O(x,y))]]
\forall z,y;[\exists x;[(~PD(z) | P(z,y) | P(x,z))]]
\forall z,y;[\exists x;[(~PD(z) | P(z,y) | ~O(x,y))]]

I don't think this splitting would yield additional OWL axioms in this particular example, but it might in other cases (e.g. someValuesFrom statements)).

in macleod/Clif.py, there is one remaining dependency on pyparsing (lines 307 and 308), which causes an error unless the pyparsing module is installed. I thought we wanted to remove that dependency.

Can we replace these lines with new parsing functionality?

We have a Readme and a docs directory which is quickly becoming outdated. Nothing keeps people from ditching software faster than realizing the installation steps and how-to guides are defunct.

In our case I think it might be better if we just update the Readme and move any official-ish looking things to the SKAI lab site. We could then put links in the Readme to redirect there for additional information if needed.

With the latest commit (59e551a), the following error gets thrown when a cl-import statement contains an error (or wrong path) after Parse w/ Imports is selected in the GUI:

'NoneType' object has no attribute 'basepath'

The traceback in the console/terminal:

Traceback (most recent call last): File "/Users/cchui/Documents/GitHub/macleod/macleod/gui/gui_beta/gui_threads.py", line 45, in run self.path) File "/Users/cchui/Documents/GitHub/macleod/macleod/parsing/Parser.py", line 538, in parse_file ontology.resolve_imports(resolve) File "/Users/cchui/Documents/GitHub/macleod/macleod/Ontology.py", line 110, in resolve_imports new_ontology = Parser.parse_file(subbed_path, sub, base, resolve) File "/Users/cchui/Documents/GitHub/macleod/macleod/parsing/Parser.py", line 538, in parse_file ontology.resolve_imports(resolve) File "/Users/cchui/Documents/GitHub/macleod/macleod/Ontology.py", line 111, in resolve_imports new_ontology.basepath = self.basepath AttributeError: 'NoneType' object has no attribute 'basepath'

An example theory where this error occurred was in http://colore.oor.net/most/most.clif which had the incorrect nested import inside http://colore.oor.net/most/most_ringbond.clif:
(cl-imports http://colore.oor.net/most/most_group_definitions.clif)
was corrected to
(cl-imports http://colore.oor.net/most/definitions/most_group_definitions.clif)

A more helpful display in the GUI to the user would be to ask them to check the import statements.

@Fxhnd I pulled the DL changes into the master branch so that I could take advantage of the constants distinction. However, I found that the analyze_logicals method will crash when the axiom has a function in it.

At the moment, I commented out the call to analyze_logicals and left a TODO note above it. At the moment, the editor doesn't know the difference between constants and variables until this works

Parser.py doesn't support "if X then Y", instead it does "if X Y", where X and Y are axioms. @thahmann said in an email that it SHOULD be "if X then Y" and to throw an error otherwise. However, a lot of things in that email aren't the case anymore.

Just looking to get some guidance before I change anything.

When extracting variables in clif.py [get_sentences_from_file] for parsing make sure to uniquely identify each variable across all sentences.

Use code from clif.py [sentence_to_tptp] as an example of what happens.

initially proposed, but currently not implemented:
SubClassOf(C ObjectHasSelf(R)) has FF-PCNF form \forall x [-C(x) | R(x, x)]
and
SubClassOf(ObjectHasSelf(R) C) has FF-PCNF form \forall x [-R(x, x) | C(x)]

Class and property symbols should always appear in the OWL output regardless if they appear in a matching pattern or not. This would guarantee a minimal working OWL ontology is produced.

Somewhere, somehow, the path management for resolving files related to the old tasks is still all wonky. If you want to run bin/check_consistency.py you'll need to actually be in the top level of the qs/ directory (e.g. You command has to look like:

python3 /path/to/macleod/bin/check_consistency.py multidim_space_codi/codi.clif

This should go away while porting the tasks to the new object structure. But that doesn't have a defined timeline so this is here as a sort of, "How do I?"

At the current moment the Parser works overtime because no effort is made to reuse already tokenized/parsed files. Speed-wise it's still faster than the previous implementation (can tokenize/parse/import all of voids_extended.clif in under 8 seconds with output) even with the multitude of duplicate imports.

Don't know the exact way forward here, but marking it down so we're aware.

Some of the commands in README.md don't work.
In the installation section, the second code block should be

# On Linux hosts with Python3 installed 
python3 -m venv ve && . ve/bin/activate

(venv is missing and it should be activate, not active)

And in the usage section, second code block, the --tptp flag is missing a -:

[rob@demo]$ parse_clif -f C:/Users/torsten/GitHub/colore/ontologies/multidim_space_dim/dim_prime_linear.clif -tptp --resolve

I think this is macOS-specific when it comes to multithreading/multiprocessing, but when utilizing the updated binaries for paradox (https://github.com/nick8325/equinox) and vampire (https://github.com/vprover/vampire) that were compiled from source, the following error is thrown:

The process has forked and you cannot use this CoreFoundation functionality safely. You MUST exec().
Break on __THE_PROCESS_HAS_FORKED_AND_YOU_CANNOT_USE_THIS_COREFOUNDATION_FUNCTIONALITY___YOU_MUST_EXEC__() to debug.

Added screenshot:

A workaround for this is to directly call the binaries in the terminal with the tptp files to do further analysis.

I'm not sure if this is something that can be fixed by modifying Macleod's code to handle processing applications outside of the GUI. I've only noticed this with Paradox and Vampire, no issues with calls to Prover9 and Mace4 with gui_beta/gui_main.py

There still exist functionality of the common logic interchange format that isn't valid against the current BNF. cl-domain is an example.

PyWin32 and wmi are used to get data from Windows based systems on the status of launched reasoners. It looks like this is only used at the moment to get the cputime for a reasoner process.

Looks at swapping it out with pip installable psutil library

If a file is not encoded with charset us-ascii the tokenization portion of the parser doesn't recognize anything. Easiest workaround is to just convert the file, have tried adding the lex.lex(reflags=re.UNICODE) to no avail.

Relevant Links:
Check encoding
Change encoding

As discussed previously, discard gui_alpha and make move everything in gui_beta up to make it THE only available GUI (maybe call it gui_main).

QObject::connect cannot queue arguments of type QTextCursor
Make sure qTextCursor is registered using qRegisterMetaType().

I believe this is a threading error, not sure.

Installation has become easier because of the wheel, but Macleod still doesn't, "Just Work" immediately after install. This could be simplified by setting some safe cross-platform defaults in the configuration and then adopting a setup where a user-supplied config file overrides the default behaviour if needed.

1. Change how Macleod searches for and uses the provers
   • Search for the application name on the PATH environment variable
   • If the name is found then assume it is active by default
   • Default some values, using minimal system resources, for each application
2. Change how Macleod resolves imports relative to other files
   1. Standard search paths
      * Documented standard search order people can reference (e.g. cmake) and build their workflow around
      * Begin search for imports relative to current file or current working directory
      * Continually search folders higher in filesystem until some stopping point (e.g. marker file, max_limit, etc)
      * Configuration values accept HINTS of directories to search first prior to the tiered search upwards
      * Add COLORE (https://github.com/gruninger/colore), OntoHub (https://ontohub.org/) well known URIs
      * Configuration accepts additional URIs for import parsing
3. Allow users to manually override each setting via their own config file given by some file following some standard location (maybe ~/.macleod, %APPDATA%, XDG standard, etc)
4. Both CLI entrypoints and the GUI should accept a config file as an optional argument and/or support overriding individual parameters via the command line.

Hi @thahmann / @Fxhnd / @evanmrsampson,

I might be missing some steps here to get macleod running on Python3, just wondering if any of you can help troubleshoot?

The older macleod Python2 scripts I have from 2016 (possibly from this commit or older: https://github.com/thahmann/macleod/tree/fa5c900afdb46b34be85865b07ad68b0a520d09b) run without issues (give or take, there's an I/O logging error on my copy that gets thrown but it doesn't seem to affect anything when I run the scripts for CLIF -> Prover9 translation):

Here's my current setup:

• OS X Yosemite (10.10.5) on Macbook Pro
• Python 3.6.4
• pip and pip3 are installed, along with texttable
• macleod Python3 scripts are on my Desktop since I don't want to mix it with the Python2 version
• followed a similar setup to the Python2 version of the scripts with modifying the macleod_mac.conf file and making sure Prover9 and Vampire binaries are in the provers/ folder
• added the macleod directory to the PYTHONPATH variable

I'm getting the following error:

The README lacks instructions on what is needed for the Python3 version (since setup.py is there) so I assumed it was a similar setup with the Python2 version of macleod.. I'm not sure if it's just a result of conflicting python/python3 and pip/pip3 packages or a relative vs. absolute path error that python3 can't find the macleod module.

If you can help out, it'd be greatly appreciated.

Thanks,
Carmen

See for example here:

Same for properties, but not individuals. Should we take a similar approach for individuals (constants): to declare all of them even those not in any pattern?

something is off, it seems like the outer universal quantifier is lost and then during PCNF creation, an existential is introduced (note that the original file contained a biconditional, though this is now changed to a conditional only):

C:\Users\torsten\GitHub\colore\ontologies\multidim_mereotopology_codi\definitions\areal_region.clif
Axiom: \forall x;[((~ArealRegion(x) | \forall y;[((~Curve(y) | Covers(x,y)) & (Covers(x,y) | Curve(y)))]) & (\forall y;[((~Curve(y) | Covers(x,y)) & (~Covers(x,y) | Curve(y)))] | ArealRegion(x)))] from C:\Users\torsten\GitHub\colore\ontologies\multidim_mereotopology_codi\definitions\areal_region.clif
((((~Covers(z,y) | Curve(y)) & (~Curve(y) | Covers(z,y))) | ~ArealRegion(z)) & ((Covers(z,x) & ~Curve(x)) | (Curve(x) & ~Covers(z,x)) | ArealRegion(z)))
FF-PCNF: \forall z,y;[\exists x;[((~ArealRegion(z) | ~Covers(z,y) | Curve(y)) & (~ArealRegion(z) | ~Curve(y) | Covers(z,y)) & (Covers(z,x) | ArealRegion(z) | Curve(x)) & (ArealRegion(z)) & (~Curve(x) | ArealRegion(z) | ~Covers(z,x)))]]

• yielded: \forall y,z;[(~ArealRegion(z) | ~Covers(z,y) | Curve(y))]
  • pattern all_values
• yielded: \forall y,z;[(~ArealRegion(z) | ~Curve(y) | Covers(z,y))]
• yielded: \forall z;[\exists x;[(Covers(z,x) | ArealRegion(z) | Curve(x))]]
• yielded: \forall z;[(ArealRegion(z))]
  • pattern universe
• yielded: \forall z;[\exists x;[(~Curve(x) | ArealRegion(z) | ~Covers(z,x))]]

Some of the clif files have a comment header in the form:
/** AUTOMATICALLY CREATED BY MACLEOD ON Fri Oct 14 11:08:16 2016**/

The grammar doesn't have this kind of comment defined so we should probably add that in at some point.

Example can be found in:
multidim_space_codi/consistency/sc_nontrivial.clif

At the current moment the repr function just recursively calls repr on it's list of imports and axioms. The result is basically a DFS through the import tree that, while cool to watch, is not very helpful when visually parsing it.

It would be better to mimic the approach used in the previous version where we first accumulate all the imports then print them. This is closely related to the other ticket about possibly reducing the duplicate imports.

With the Python3 version of Macleod, the GUI output is somewhat misleading when dealing with symbols like + or - in both the Common Logic comments and axioms.

For example, opening http://colore.oor.net/psl_core/psl_core.clif will trigger the following output in the latest version of Macleod:

This doesn't affect the translation into LADR or TPTP but the output in the GUI is misleading.

In comparison, with the Python2 version of macleod, this error message doesn't appear in the GUI output:

This only affects the following CLIF files:

• http://colore.oor.net/psl_core/psl_core.clif
• http://colore.oor.net/psl_core/psl_core_root.clif
• and possibly any other CLIF files that have symbols in their constants

in the editor, use the functionality for finding constants from the "ontology object" in the object structure (implemented by @Fxhnd in the DL branch)

When Parser.py generates the parsetab file it throws a warning about a shift/reduce conflict. Essentially this means that the grammar as defined has one situation where the parser wouldn't know if it should shift another character or reduce to an already matching rule. I don't think it's a problem because the default behavior is that the parser will shift -- which for this grammar should work all the time as a solution.

It'd still be good to clean up the grammar and document it though.

In psl_core.clif, there is the following axiom:

(forall (x occ t) (if (participates_in x occ t) (and (exists_at x t) (is_occurring_at occ t))))

The latest commit to macleod will not translate this axiom due to the fact that exists is a keyword in the translation scripts. It will not parse exists_at with the underscore -- even renaming to existsAt will cause the GUI to throw a token error:

Error at line 129! Unexpected Token: '_̲at̲'
Error at line 151! Unexpected Token: '_̲at̲'

I would believe this error would be thrown if there are other relations with names that start with any of the quantifier keywords.

With the upgrade to Python3 it may be possible to drop our requirement for these libraries. I believe they're currently used to be able to get detailed process information on the prover processes when they're running.

If the Python standard libraries can't achieve it, it may still be possible by shelling out to Powershell on Windows.

Things we need for "detailed" process information

1. Time the process has been running
2. CPU usage information
3. Memory usage information
4. Maybe something else