diff --git a/README.md b/README.md index dc96fd03..6ef4106e 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@
-
Java Geometry Expert
+
Java Geometry Expert

JGEX is a software which combines dynamic geometry software (DGS), automated geometry theorem prover (GTP) and our approach for visually dynamic presentation of proofs. As a dynamic geometry software, JGEX can be used to build dynamic visual models to assist teaching and learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic models which can do reasoning themselves. As a tool for dynamic presentation of proofs, JGEX is a valuable for teachers and students to write and present proofs of geometry theorems with various dynamic visual effects.

  1. JGEX is a powerful software for geometric reasoning. Within its domain, it invites comparison with the best of human geometry provers. It implements most of the effective methods for geometric reasoning introduced in the past twenty years, including the deductive base method, Wu's method, and the full-angle method, etc. With these methods, users may automated prove geometry theorems, to discover new properties of theorems, and to generate readable proofs for many geometry theorems.
    2. @@ -20,22 +20,22 @@

    By a dynamic geometry we simply mean a study of the parts of space andtheir relations to one another while they are in motion and changing.

    The drawing part of JGEX allows the user to construct the diagram interactively and manipulate the diagram in a dynamic way, so JGEX is first a DGS. Starting from free points, the user can create elements which is dependent on existed elements. With the mouse, the user can place points, draw lines, introduce marks, etc. In this way, the diagram is constructed step by step. Much more important is the fact that the user can explore the dynamic nature of the diagram. The user can drag part of the diagram with mouse and see immediately how the diagram changes accordingly. However, JGEX has its distinctive features comparing to the three commercial geometry drawing systems.

    -

    See Detail >>>

    +

    See Detail >>>

    2. An Automated Geometry Theorem Prover

    Wu's method, the Full Angle Method and the Deductive Database Method based on Full Angle are implemented in JGEX as reasoning and proving tool.

    -

    See Detail >>>

    +

    See Detail >>>

    3. A Tool for Visual Presentation of Proofs

    The part of visual presentation of proofs makes JGEX most distinctive from other geometry drawing systems on one side, and from other geometry reasoning systems, including our previous versions of GEX, on the other side. It is based on our work on automated generation of readable proofs and on our approach to geometric drawing.

    However, as a first step, instead of automated generation of visual presentations of proofs, we implement the manual input method for creating visual presentations of proofs. This gives us first-hand experience with the approach we propose. It is also an important preparation for our future work on the proof checker. Especially, we have a collection of over 100 examples created manually with JGEX. We collect mainly those examples that do not mix algebraic expressions or computations with the geometry diagrams.

    -

    See Detail >>>

    +

    See Detail >>>

     

    See Also:

     

    @@ -53,20 +53,20 @@

    5. The interface of JGEX

    -


    +


    Some interesting animations

    - - - - - - + + + + + + - @@ -90,6 +90,7 @@ some features in this version:
  2. Jorge Cassio (Portuguese translation)
  3. Noah Dana-Picard (French and Hebrew translation)
  4. Ines Ganglmayr (German translation) +
  5. Philip Hallwirth (Code cleanup, CheerpJ port)
  6. Benedek Kovács (Localization support)
  7. Zoltán Kovács (Hungarian and German translations)
  8. Predrag Janičić (Serbian translation) diff --git a/build.gradle b/build.gradle index 629714e0..f2a5fa8b 100644 --- a/build.gradle +++ b/build.gradle @@ -31,7 +31,7 @@ apply plugin: 'io.github.fvarrui.javapackager.plugin' // Global settings: group = 'io.github.kovzol' -ext.softwareVersion = '0.86' +ext.softwareVersion = '0.87' // These are default settings based on Gradle's standard layout: ext.poDir = 'src/main/po' diff --git a/snapcraft.yaml b/snapcraft.yaml index 09a4298f..37480102 100644 --- a/snapcraft.yaml +++ b/snapcraft.yaml @@ -1,8 +1,8 @@ name: jgex architectures: - build-on: amd64 -base: core18 -version: '0.86' +base: core20 +version: '0.87' summary: Java Geometry Expert description: | JGEX combines dynamic geometry software, @@ -16,11 +16,11 @@ confinement: strict apps: jgex: extensions: - - gnome-3-28 - command: $SNAP/bin/jgex + - gnome-3-38 + command: bin/jgex environment: JAVA_HOME: $SNAP/usr/lib/jvm/java-11-openjdk-amd64 - PATH: $JAVA_HOME/jre/bin:$PATH + PATH: $JAVA_HOME/bin:$PATH JAVA_OPTS: -Djava.util.prefs.userRoot="$SNAP_USER_DATA" LIBGL_DRIVERS_PATH: $SNAP/usr/lib/x86_64-linux-gnu/dri LC_ALL: C.UTF-8 @@ -34,24 +34,24 @@ parts: jgex: build-packages: [gettext, openjdk-11-jdk] source: https://github.com/kovzol/Java-Geometry-Expert.git - plugin: gradle + plugin: dump source-type: git override-build: | snapcraftctl build - ./gradlew installDist - mkdir -p $SNAPCRAFT_PART_INSTALL/usr/share/jgex - cp -a build/install/jgex/lib/*.jar $SNAPCRAFT_PART_INSTALL/usr/share/jgex - mkdir -p $SNAPCRAFT_PART_INSTALL/root - cp -a build/install/jgex/bin/examples $SNAPCRAFT_PART_INSTALL/root - cp -a build/install/jgex/bin/help $SNAPCRAFT_PART_INSTALL/root - cp -a build/install/jgex/bin/import $SNAPCRAFT_PART_INSTALL/root - cp -a build/install/jgex/bin/rules $SNAPCRAFT_PART_INSTALL/root - echo "#!/bin/bash" > $SNAPCRAFT_PART_INSTALL/bin/jgex - echo "JGEX_WD=~/.jgex # working directory" >> $SNAPCRAFT_PART_INSTALL/bin/jgex - echo "test -d \$JGEX_WD || (mkdir -p \$JGEX_WD; cd \$SNAP/root; cp -a -u * \$JGEX_WD)" >> $SNAPCRAFT_PART_INSTALL/bin/jgex - echo "cd \$JGEX_WD" >> $SNAPCRAFT_PART_INSTALL/bin/jgex - echo "java -cp \$SNAP/usr/share/jgex/\\* wprover.GExpert \$*" >> $SNAPCRAFT_PART_INSTALL/bin/jgex - chmod 755 $SNAPCRAFT_PART_INSTALL/bin/jgex + ./gradlew installDist && \ + mkdir -p ../install/usr/share/jgex && \ + cp -a build/install/jgex/lib/*.jar ../install/usr/share/jgex && \ + mkdir -p ../install/root && \ + cp -a build/install/jgex/bin/examples ../install/root && \ + cp -a build/install/jgex/bin/help ../install/root && \ + cp -a build/install/jgex/bin/import ../install/root && \ + cp -a build/install/jgex/bin/rules ../install/root && \ + echo "#!/bin/bash" > ../install/bin/jgex && \ + echo "JGEX_WD=~/.jgex # working directory" >> ../install/bin/jgex && \ + echo "test -d \$JGEX_WD || (mkdir -p \$JGEX_WD; cd \$SNAP/root; cp -a -u * \$JGEX_WD)" >> ../install/bin/jgex && \ + echo "cd \$JGEX_WD" >> ../install/bin/jgex && \ + echo "java -cp \$SNAP/usr/share/jgex/\\* wprover.GExpert \$*" >> ../install/bin/jgex && \ + chmod 755 ../install/bin/jgex stage-packages: - bash @@ -72,3 +72,4 @@ parts: snapcraftctl prime rm -f usr/lib/jvm/java-11-openjdk-*/lib/security/blacklisted.certs rm -fr jar + diff --git a/src/index.html b/src/index.html index 2296ffb4..b0ed6279 100644 --- a/src/index.html +++ b/src/index.html @@ -11,7 +11,7 @@ (async function () { await cheerpjInit({ version: 11 , enableDebug: true}); cheerpjCreateDisplay(1400, 800); - await cheerpjRunJar("/app/Java-Geometry-Expert-0.86.jar"); + await cheerpjRunJar("/app/Java-Geometry-Expert-0.87.jar"); })(); diff --git a/src/main/java/wprover/PanelProve.java b/src/main/java/wprover/PanelProve.java index 73891961..bdf59e30 100644 --- a/src/main/java/wprover/PanelProve.java +++ b/src/main/java/wprover/PanelProve.java @@ -1669,7 +1669,7 @@ String setNode(Cond co) { ret += ", tooltip = \" \""; // do not show any tooltip } // The files Rule??.jpg are located in the folder web: - String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/docs/web/Rule" + rule + ".jpg?raw=true"; + String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/main/resources/docs/web/Rule" + rule + ".jpg?raw=true"; ret += ", style = \"" + s + "\", shape = " + f + ", fillcolor = \"" + c + "\"" + ", URL=\"" + url + "\"" + "];\n"; @@ -1702,7 +1702,7 @@ Node graphvizNode(Cond co) { // For some reason, this does not work, we get // an error org.apache.batik.dom.util.SAXIOException: Invalid byte 1 of 1-byte UTF-8 sequence. // FIXME. - // String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/docs/web/Rule" + rule + ".jpg?raw=true"; + // String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/main/resources/docs/web/Rule" + rule + ".jpg?raw=true"; n = Node.builder().shape(s).table(table().border(0).bgColor(c). cellBorder(0).cellSpacing(0).cellPadding(6).href(url).tooltip(tooltipstring). tr(td().color(c).text(co.getNo() + ") " + co.getText())). diff --git a/src/main/java/wprover/Version.java b/src/main/java/wprover/Version.java index 3bc74b97..3eeb4bc4 100644 --- a/src/main/java/wprover/Version.java +++ b/src/main/java/wprover/Version.java @@ -6,7 +6,7 @@ */ public class Version { - private static String sversion = "0.86"; + private static String sversion = "0.87"; private static String data = "2024-11-26"; private static String project = "Geometry Expert"; diff --git a/src/test/import-ggb-prove-gdd-export-gv-png b/src/test/import-ggb-prove-gdd-export-gv-png index b119490e..d11cdfb3 100755 --- a/src/test/import-ggb-prove-gdd-export-gv-png +++ b/src/test/import-ggb-prove-gdd-export-gv-png @@ -1,6 +1,6 @@ #!/bin/bash -# This script runs all .ggb files from ../docs/import/ggb-benchmarks, -# proves them via the GDD method and saves the proof tree as .gv and .png in ../docs. +# This script runs all .ggb files from ../main/resources/docs/import/ggb-benchmarks, +# proves them via the GDD method and saves the proof tree as .gv and .png in ../main/resources/docs. # Run this script with # xvfb-run -a -s "-screen 0 1280x800x24" ./import-ggb-prove-gdd-export-gv-png @@ -11,7 +11,7 @@ # "snap" uses the snapcraft installation and considered therefore faster. -BENCHMARKS_FOLDER=../docs/import/ggb-benchmarks # this may be changed on demand +BENCHMARKS_FOLDER=../main/resources/docs/import/ggb-benchmarks # this may be changed on demand TIMEOUT=5 # JGEX forgets to quit sometimes, this timeout ensures proper exit test -x $BENCHMARKS_FOLDER || { @@ -61,21 +61,21 @@ for FULLNAME in `find $BENCHMARKS_FOLDER -name '*.ggb' | sort`; do GV=$GV_DIR/$NAME.gv rm -f $GV # remove a possible successful export from a previous run if [ "$1" = "snap" ]; then - /bin/time -o ../docs/$NAME.txt /usr/bin/timeout -k $((TIMEOUT+1)) $TIMEOUT jgex -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME > ../docs/$NAME.log 2>&1 + /bin/time -o ../main/resources/docs/$NAME.txt /usr/bin/timeout -k $((TIMEOUT+1)) $TIMEOUT jgex -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME > ../main/resources/docs/$NAME.log 2>&1 else pushd ../.. >/dev/null RUNTIME=`pwd`/build/install/jgex/bin/Java-Geometry-Expert - /bin/time -o src/docs/$NAME.txt /usr/bin/timeout -k $((TIMEOUT+1)) $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME > src/docs/$NAME.log 2>&1 + /bin/time -o src/main/resources/docs/$NAME.txt /usr/bin/timeout -k $((TIMEOUT+1)) $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME > src/main/resources/docs/$NAME.log 2>&1 popd >/dev/null fi - PROBLEM=`cat ../docs/$NAME.log | grep "Unimplemented\|Unidentified\|Unsupported\|Exception" | grep -v "org.graphper.draw.ExecuteException" | head -1` + PROBLEM=`cat ../main/resources/docs/$NAME.log | grep "Unimplemented\|Unidentified\|Unsupported\|Exception" | grep -v "org.graphper.draw.ExecuteException" | head -1` test -s $GV && { MD5SUM=`md5sum $GV | cut -f1 -d" "` if [ "$MD5SUM" = "d872444bcef19cb5462bb9a4fb4e9fb3" -o "$MD5SUM" = "3c964068bf7b811e7570449adc59af0e" -o "$MD5SUM" = "dd5ece2abd55b6f9b27df4df90e66fdf" ]; then echo -e "$WARNING_COLOR$NAME unsuccessful: empty gv tree, $PROBLEM$RESUME_COLOR" BAD=$((BAD+1)) else - dot -Tpng $GV > ../docs/$NAME.png + dot -Tpng $GV > ../main/resources/docs/$NAME.png LENGTH=`cat $GV | wc -l` echo -e "$CORRECT_COLOR$NAME successful: $LENGTH lines of gv output$RESUME_COLOR" GOOD=$((GOOD+1)) diff --git a/src/test/prove-gdd-export-gv-svg b/src/test/prove-gdd-export-gv-svg index ac39dd1a..b1ecabcd 100755 --- a/src/test/prove-gdd-export-gv-svg +++ b/src/test/prove-gdd-export-gv-svg @@ -1,6 +1,6 @@ #!/bin/bash -# This script runs all .gex files from ../docs/examples/6_GDD_FULL, -# proves them via the GDD method and saves the proof tree as .gv and .svg in ../docs. +# This script runs all .gex files from ../main/resources/docs/examples/6_GDD_FULL, +# proves them via the GDD method and saves the proof tree as .gv and .svg in ../main/resources/docs. # Run this script with # xvfb-run -a -s "-screen 0 1280x800x24" ./prove-gdd-export-gv-svg @@ -14,8 +14,8 @@ cd ../.. RUNTIME=`pwd`/build/install/jgex/bin/Java-Geometry-Expert MYDIR=`pwd` -for FULLNAME in `find src/docs/examples/6_GDD_FULL -name '*.gex' `; do +for FULLNAME in `find src/main/resources/docs/examples/6_GDD_FULL -name '*.gex' `; do NAME=`basename $FULLNAME .gex` - /bin/time -o src/docs/$NAME.txt /usr/bin/timeout -k $TIMEOUT $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME - dot -Tsvg $NAME.gv > src/docs/$NAME.svg + /bin/time -o src/main/resources/docs/$NAME.txt /usr/bin/timeout -k $TIMEOUT $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME + dot -Tsvg $NAME.gv > src/main/resources/docs/$NAME.svg done


    9. +



    A Manually Created Proof for Pythagoras Theorem.