Merge pull request #15 from sucksome/master

Aris for Qt and WebAssembly

.gitignore

@@ -13,9 +13,12 @@ build-aux
 *.o
 src/aris
 src/.deps
+build*
+libxml2
+qt/*.user
 
 # Generated Documentation
 doc/aris/*.html
 doc/aris.info
 doc/stamp-vti
-doc/version.texi
+doc/version.texi

AUTHORS

@@ -10,3 +10,7 @@ The following people contributed to GNU Aris,
 and their time and effort are greatly appreciated:
 
 Ian Dunn <[email protected]>
+Kovács Zoltán <[email protected]>
+Saksham Attri <[email protected]>
+Alexander Thaller <[email protected]>
+Andreas Ebetshuber <[email protected]>

CMakeLists.txt

@@ -3,7 +3,7 @@ project(aris C)
 
 set(PACKAGE_NAME "GNU Aris")
 set(PACKAGE "aris")
-set(ARIS_VERSION "2.2")
+set(ARIS_VERSION "3.0")
 set(PACKAGE_BUGREPORT "[email protected]")
 
 set(CMAKE_C_STANDARD 11)

NEWS

@@ -7,6 +7,16 @@ This NEWS file records important changes.
   notice and this notice are preserved.
 
 
+3.0
+
+  * Added a qt version.
+
+  * Added support for WebAssembly compilation.
+
+  * Fixed up subproof referencing bugs.
+
+  * Fixed up On-Screen Keyboard bugs on gtk build.
+
 2.2
 
   * Added undo/redo functionality.

README.md

@@ -1,36 +1,45 @@
 
-### GNU Aris distribution
+# GNU Aris
 
 GNU Aris is a logical proof program that provides support for propositional and predicate logic, Boolean algebra, and arithmetical logic in the form of abstract sequences (seqlog). This software is distributed under the GNU General Public License.
 
---------------------
 Copyright (C) 2012, 2013 Ian Dunn
 
 Copying and distribution of this file, with or without modification, are permitted in any medium without royalty provided the copyright
 notice and this notice are preserved.
 
-----
-### Table of Contents
+## Table of Contents
 - [Installation Guide](#installation-guide)
-  - [Build GNU Aris through source](#build-gnu-aris-through-source)
+  - [gtk version](#gtk-version)
+  - [qt version](#qt-version)
+  - [WebAssembly](#webassembly)
 - [Contributing Guide](#contributing-guide)
   - [Getting Started](#getting-started)
   - [How to Contribute](#how-to-contribute)
   - [Report a Bug](#report-a-bug)
 - [Contact Us](#contact-us)
 - [References](#references)
 
-### Installation Guide
-#### Build GNU Aris through source
-To build GNU Aris through source, follow the instructions given below. This should work on Linux, Mac or Windows (by using, for example, the MSYS2 toolchain and its MINGW64 environment):
+## Installation Guide
+Check under `Releases` for Linux/Windows bundles and `AppImages` or visit our [website](https://matek.hu/zoltan/aris) .
 
-1. Clone the Aris repository from https://github.com/kovzol/aris using the command `git clone https://github.com/kovzol/aris`.
+Else, to build GNU Aris through source, follow the instructions given below. This should work on Linux, Mac or Windows (by using, for example, the MSYS2 toolchain and its MINGW64 environment):
 
-2. Create a directory named **build** by entering `mkdir build`.
+Clone/Download the repository. For example:
+   ```
+   git clone https://github.com/kovzol/aris
+   ```
 
-3. Change your working directory to this folder: `cd build`.
+### gtk version
 
-3. Run the command `cmake ..`. You should see something like this:
+1. Follow the steps:
+```
+mkdir build
+cd build
+cmake ..
+```
+
+2. You should see something like this:
 ```
 -- The C compiler identification is GNU 11.3.0
 -- Detecting C compiler ABI info
@@ -44,10 +53,10 @@ To build GNU Aris through source, follow the instructions given below. This shou
 --   Found gtk+-3.0, version 3.24.33
 -- Configuring done
 -- Generating done
--- Build files have been written to: /home/kovzol/workspace/aris/b
+-- Build files have been written to: /home/abc/workspace/aris/build/
 ```
 
-4. Run the command `make`. You should see something like this at the end of the process:
+3. Run the command `make`. You should see something like this at the end of the process:
 ```
 [ 88%] Building C object CMakeFiles/aris.dir/src/undo.c.o
 [ 92%] Building C object CMakeFiles/aris.dir/src/var.c.o
@@ -56,13 +65,90 @@ To build GNU Aris through source, follow the instructions given below. This shou
 [100%] Built target aris
 ```
 
-5. Launch GNU Aris using `./aris`.
+4. Launch using `./aris`.
+
+For further instructions on building and installation ( without `cmake`), refer to the [INSTALL](INSTALL) file.
+
+#### Snap Installation
+
+To install GNU Aris through snap, visit https://snapcraft.io/aris and find the required distribution details according to your system.
+
+### qt version
+#### Using `cmake`
+
+##### Linux
+Run the following inside `aris/` :
+```
+cmake -S qt/ -B build-qt/ -DCMAKE_GENERATOR:STRING=Ninja -DCMAKE_BUILD_TYPE:STRING=Release
+cmake --build build-qt/ --target all
+```
+This should generate a binary `aris-qt` inside `build-qt/` , it can be run with `./aris-qt` or you can install to `/usr/local` with:
+```
+cd build-qt/ && cmake -P cmake_install.cmake
+```
+To uninstall:
+```
+cd build-qt/ && xargs rm < install_manifest.txt
+```
+
+##### Windows (with MINGW)
+
+Run the following inside `aris/`:
+```
+mkdir build
+cd build
+cmake -G "MinGW Makefiles" ..
+mingw32-make -j4
+```
 
-For further instructions on building and installation, refer to the INSTALL file.
+#### Using `qmake`
 
-#### Run a precompiled binary of GNU Aris through snap
+Run the following inside `aris/` with appropriate `path/to/qmake`:
+```
+mkdir build-qt
+cd build-qt
+path/to/qmake -o Makefile ../qt/aris-qt.pro -spec linux-g++ CONFIG+=qtquickcompiler
+```
+This should generate a binary `aris-qt` inside `build-qt/` , it can be run with `./aris-qt` .
+
+### WebAssembly
+
+To build to WebAssembly, `Qt 6.5` and `emscripten` version `3.1.25` are required.
+Also, since `emscripten` doesn't have support for `libxml2` yet, it would need to be compiled from source.
+
+Follow these steps (after cloning libxml2) to compile `libxml2` :
+```
+mkdir build
+cd libxml2 && autoreconf -if -Wall
+cd ../build 
+path/to/emconfigure ../libxml2/configure --with-http=no --with-ftp=no --with-python=no --with-threads=no --enable-shared=no
+path/to/emmake make
+path/to/emar rcs libxml2.a *.o
+```
+
+Now, inside `aris/` run the following:
+```
+mkdir libxml2
+cp path/to/above/created/libxml2.a libxml2/
+cp -r path/to/cloned-libxml2/include/libxml/ libxml2/
+```
+You can customize these paths by editing the `aris-qt.pro` file.
+
+Finally:
+
+```
+mkdir build-wasm
+cd build-wasm
+/path/to/Qt/6.5.0/wasm_singlethread/bin/qmake /path/to/aris/qt/aris-qt.pro -spec wasm-emscripten && /usr/bin/make qmake_all
+make -j $(nproc)
+```
+
+Now, run:
+```
+python -m http.server 8000
+```
+The project can be found at `http://0.0.0.0:8000/` .
 
-To install GNU Aris through snap, visit https://snapcraft.io/aris and find the required distribution details according to your system. For example, for Linux machines, use `sudo snap install aris` to install the Aris and launch it with `aris`.
 
 ### Contributing Guide
 We welcome contributions to our project and thank you for taking the time to improve it. Here are some guidelines to follow when contributing:

configure.ac

@@ -1,5 +1,5 @@
 AC_PREREQ(2.60)
-AC_INIT([GNU Aris], [2.2], [[email protected]])
+AC_INIT([GNU Aris], [3.0], [[email protected]])
 AC_CONFIG_AUX_DIR([build-aux])
 AM_INIT_AUTOMAKE
 

qt/CMakeLists.txt

@@ -0,0 +1,95 @@
+cmake_minimum_required(VERSION 3.16)
+
+project(aris-qt VERSION 0.1 LANGUAGES C CXX)
+
+set(CMAKE_AUTOMOC ON)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+add_compile_definitions(WITH_CMAKE)
+
+find_package(Qt6 6.2 REQUIRED COMPONENTS Quick Widgets QuickControls2)
+find_package(LibXml2 REQUIRED)
+
+add_executable(aris-qt
+    ../src/aio.h
+    auxconnector.h
+    connector.h
+    goaldata.h
+    goalmodel.h
+    goals-qt.h
+    ../src/interop-isar.h
+    ../src/list.h
+    ../src/process.h
+    ../src/proof.h
+    proofdata.h
+    proofmodel.h
+    ../src/rules.h
+    ../src/sen-data.h
+    ../src/sexpr-process.h
+    ../src/typedef.h
+    ../src/var.h
+    ../src/vec.h
+    ../src/aio.c
+    auxconnector.cpp
+    connector.cpp
+    goaldata.cpp
+    goalmodel.cpp
+    goals-qt.c
+    ../src/interop-isar.c
+    ../src/list.c
+    main.cpp
+    ../src/process-main.c
+    ../src/process.c
+    ../src/proof.c
+    proofdata.cpp
+    proofmodel.cpp
+    ../src/sen-data.c
+    ../src/sexpr-process-bool.c
+    ../src/sexpr-process-equiv.c
+    ../src/sexpr-process-infer.c
+    ../src/sexpr-process-misc.c
+    ../src/sexpr-process-quant.c
+    ../src/sexpr-process.c
+    ../src/var.c
+    ../src/vec.c
+)
+
+qt_add_qml_module(aris-qt
+    URI arisqt
+    VERSION 1.0
+    QML_FILES main.qml ProofArea.qml DrawerTools.qml GoalLine.qml KeyButton.qml KeyGroup.qml
+    RESOURCES
+        assets/help.png
+        assets/icon_simple.svg
+        assets/about.png
+        assets/font.png
+        assets/import.png
+        assets/boolean.png
+        assets/goal.png
+        assets/export.png
+        assets/saveas.png
+        assets/save.png
+        assets/folder.png
+        assets/new.png
+        assets/eval.png
+)
+
+set_target_properties(aris-qt PROPERTIES
+    MACOSX_BUNDLE_GUI_IDENTIFIER my.example.com
+    MACOSX_BUNDLE_BUNDLE_VERSION ${PROJECT_VERSION}
+    MACOSX_BUNDLE_SHORT_VERSION_STRING ${PROJECT_VERSION_MAJOR}.${PROJECT_VERSION_MINOR}
+    MACOSX_BUNDLE TRUE
+    WIN32_EXECUTABLE TRUE
+)
+
+target_link_libraries(aris-qt
+    PRIVATE Qt6::Quick
+    PRIVATE Qt6::Widgets
+    PRIVATE Qt6::QuickControls2
+    PUBLIC LibXml2::LibXml2
+)
+
+install(TARGETS aris-qt
+    BUNDLE DESTINATION .
+    LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
+    RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}
+)