Skip to content

Commit 0765730

Browse files
kovzolkovzol
committed
Polishing version 0.87
1 parent 0069549 commit 0765730

8 files changed

Lines changed: 55 additions & 53 deletions

File tree

‎README.md‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
<div class="wikitopline"></div>
44

55
<div class="wikitext">
6-
<div width="30%" height="90" style="width: 45%; color: rgb(0, 0, 0);"><span style="width: 280px; text-align: center; white-space: nowrap; color: rgb(0, 0, 0);"><img src="src/docs/help/images/headline.jpg" alt="Java Geometry Expert" width="218" height="117" /></span></div>
6+
<div width="30%" height="90" style="width: 45%; color: rgb(0, 0, 0);"><span style="width: 280px; text-align: center; white-space: nowrap; color: rgb(0, 0, 0);"><img src="src/main/resources/docs/help/images/headline.jpg" alt="Java Geometry Expert" width="218" height="117" /></span></div>
77
<p>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.</p>
88
<ol>
99
<li>JGEX is a powerful software for <em>geometric reasoning</em>. 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. </li>
@@ -20,22 +20,22 @@
2020
<p align="center" class="codelisting STYLE1">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.</p>
2121
</blockquote>
2222
<p> 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.</p>
23-
<p><a href="src/docs/help/dynamic_geometry_software.html">See Detail &gt;&gt;&gt;</a> </p>
23+
<p><a href="src/main/resources/docs/help/dynamic_geometry_software.html">See Detail &gt;&gt;&gt;</a> </p>
2424
<h3>2. An Automated Geometry Theorem Prover <a name="gtp" id="gtp"></a></h3>
2525
<p>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.</p>
26-
<p><a href="src/docs/help/automated_theorem_prover.html">See Detail &gt;&gt;&gt; </a></p>
26+
<p><a href="src/main/resources/docs/help/automated_theorem_prover.html">See Detail &gt;&gt;&gt; </a></p>
2727
<h3>3. A Tool for Visual Presentation of Proofs <a name="vpp" id="vpp"></a></h3>
2828
<p>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.</p>
2929
<p>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.</p>
30-
<p><a href="src/docs/help/dynamic_presentation_of_proofs.html">See Detail &gt;&gt;&gt; </a></p>
30+
<p><a href="src/main/resources/docs/help/dynamic_presentation_of_proofs.html">See Detail &gt;&gt;&gt; </a></p>
3131
<p>&nbsp;</p>
3232
<p><strong>See Also: </strong></p>
3333
<ul>
34-
<li><a title="no description" href='src/docs/help/gex_jgex.html' class='wiki'>GEX and JGEX </a></li>
35-
<li> <a title="no description" href='src/docs/help/dynamic_geometry_software.html' class='wiki'>A Dynamic Geometry Software</a></li>
36-
<li> <a title="no description" href='src/docs/help/automated_theorem_prover.html' class='wiki'>An Automated
34+
<li><a title="no description" href='src/main/resources/docs/help/gex_jgex.html' class='wiki'>GEX and JGEX </a></li>
35+
<li> <a title="no description" href='src/main/resources/docs/help/dynamic_geometry_software.html' class='wiki'>A Dynamic Geometry Software</a></li>
36+
<li> <a title="no description" href='src/main/resources/docs/help/automated_theorem_prover.html' class='wiki'>An Automated
3737
Geometry Theorem Prover</a></li>
38-
<li> <a title="no description" href='src/docs/help/dynamic_presentation_of_proofs.html' class='wiki'>A Tool for Visually Dynamic
38+
<li> <a title="no description" href='src/main/resources/docs/help/dynamic_presentation_of_proofs.html' class='wiki'>A Tool for Visually Dynamic
3939
Presentation of Proofs</a></li>
4040
</ul>
4141
<p>&nbsp;</p>
@@ -53,20 +53,20 @@
5353
</p>
5454

5555
<h3>5. The interface of JGEX <a name="vpp" id="vpp"></a></h3>
56-
<p><img src="src/docs/help/images3/jgex.gif" width="802" height="645" border="1" /><br />
56+
<p><img src="src/main/resources/docs/help/images3/jgex.gif" width="802" height="645" border="1" /><br />
5757
</p>
5858

5959
<p>Some interesting animations</p>
60-
<img src="src/docs/help/effects/st.gif" border="1" height="180" width="400" />
61-
<img src="src/docs/help/effects/cg.gif" border="1" height="180" width="400" />
62-
<img src="src/docs/help/effects/p3.gif" border="1" height="180" width="400" />
63-
<img src="src/docs/help/effects/p4.gif" border="1" height="180" width="400" />
64-
<img src="src/docs/help/effects/p5.gif" border="1" height="180" width="400" />
65-
<img src="src/docs/help/effects/p6.gif" border="1" height="180" width="400" />
60+
<img src="src/main/resources/docs/help/effects/st.gif" border="1" height="180" width="400" />
61+
<img src="src/main/resources/docs/help/effects/cg.gif" border="1" height="180" width="400" />
62+
<img src="src/main/resources/docs/help/effects/p3.gif" border="1" height="180" width="400" />
63+
<img src="src/main/resources/docs/help/effects/p4.gif" border="1" height="180" width="400" />
64+
<img src="src/main/resources/docs/help/effects/p5.gif" border="1" height="180" width="400" />
65+
<img src="src/main/resources/docs/help/effects/p6.gif" border="1" height="180" width="400" />
6666

6767
<table width="200" border="0" align="center">
6868
<tr>
69-
<td><p align="center"><img src="src/docs/help/images2/pyth1.gif" width="698" height="378" border="1" /><br />
69+
<td><p align="center"><img src="src/main/resources/docs/help/images2/pyth1.gif" width="698" height="378" border="1" /><br />
7070
<br />
7171
<strong>A Manually Created Proof for Pythagoras Theorem. </strong> </p></td>
7272
</tr>
@@ -90,6 +90,7 @@ some features in this version:
9090
<li>Jorge Cassio (Portuguese translation)
9191
<li>Noah Dana-Picard (French and Hebrew translation)
9292
<li>Ines Ganglmayr (German translation)
93+
<li>Philip Hallwirth (Code cleanup, CheerpJ port)
9394
<li>Benedek Kovács (Localization support)
9495
<li>Zoltán Kovács (Hungarian and German translations)
9596
<li>Predrag Janičić (Serbian translation)

‎build.gradle‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ apply plugin: 'io.github.fvarrui.javapackager.plugin'
3131

3232
// Global settings:
3333
group = 'io.github.kovzol'
34-
ext.softwareVersion = '0.86'
34+
ext.softwareVersion = '0.87'
3535

3636
// These are default settings based on Gradle's standard layout:
3737
ext.poDir = 'src/main/po'

‎snapcraft.yaml‎

Lines changed: 21 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
name: jgex
22
architectures:
33
- build-on: amd64
4-
base: core18
5-
version: '0.86'
4+
base: core20
5+
version: '0.87'
66
summary: Java Geometry Expert
77
description: |
88
JGEX combines dynamic geometry software,
@@ -16,11 +16,11 @@ confinement: strict
1616
apps:
1717
jgex:
1818
extensions:
19-
- gnome-3-28
20-
command: $SNAP/bin/jgex
19+
- gnome-3-38
20+
command: bin/jgex
2121
environment:
2222
JAVA_HOME: $SNAP/usr/lib/jvm/java-11-openjdk-amd64
23-
PATH: $JAVA_HOME/jre/bin:$PATH
23+
PATH: $JAVA_HOME/bin:$PATH
2424
JAVA_OPTS: -Djava.util.prefs.userRoot="$SNAP_USER_DATA"
2525
LIBGL_DRIVERS_PATH: $SNAP/usr/lib/x86_64-linux-gnu/dri
2626
LC_ALL: C.UTF-8
@@ -34,24 +34,24 @@ parts:
3434
jgex:
3535
build-packages: [gettext, openjdk-11-jdk]
3636
source: https://github.com/kovzol/Java-Geometry-Expert.git
37-
plugin: gradle
37+
plugin: dump
3838
source-type: git
3939
override-build: |
4040
snapcraftctl build
41-
./gradlew installDist
42-
mkdir -p $SNAPCRAFT_PART_INSTALL/usr/share/jgex
43-
cp -a build/install/jgex/lib/*.jar $SNAPCRAFT_PART_INSTALL/usr/share/jgex
44-
mkdir -p $SNAPCRAFT_PART_INSTALL/root
45-
cp -a build/install/jgex/bin/examples $SNAPCRAFT_PART_INSTALL/root
46-
cp -a build/install/jgex/bin/help $SNAPCRAFT_PART_INSTALL/root
47-
cp -a build/install/jgex/bin/import $SNAPCRAFT_PART_INSTALL/root
48-
cp -a build/install/jgex/bin/rules $SNAPCRAFT_PART_INSTALL/root
49-
echo "#!/bin/bash" > $SNAPCRAFT_PART_INSTALL/bin/jgex
50-
echo "JGEX_WD=~/.jgex # working directory" >> $SNAPCRAFT_PART_INSTALL/bin/jgex
51-
echo "test -d \$JGEX_WD || (mkdir -p \$JGEX_WD; cd \$SNAP/root; cp -a -u * \$JGEX_WD)" >> $SNAPCRAFT_PART_INSTALL/bin/jgex
52-
echo "cd \$JGEX_WD" >> $SNAPCRAFT_PART_INSTALL/bin/jgex
53-
echo "java -cp \$SNAP/usr/share/jgex/\\* wprover.GExpert \$*" >> $SNAPCRAFT_PART_INSTALL/bin/jgex
54-
chmod 755 $SNAPCRAFT_PART_INSTALL/bin/jgex
41+
./gradlew installDist && \
42+
mkdir -p ../install/usr/share/jgex && \
43+
cp -a build/install/jgex/lib/*.jar ../install/usr/share/jgex && \
44+
mkdir -p ../install/root && \
45+
cp -a build/install/jgex/bin/examples ../install/root && \
46+
cp -a build/install/jgex/bin/help ../install/root && \
47+
cp -a build/install/jgex/bin/import ../install/root && \
48+
cp -a build/install/jgex/bin/rules ../install/root && \
49+
echo "#!/bin/bash" > ../install/bin/jgex && \
50+
echo "JGEX_WD=~/.jgex # working directory" >> ../install/bin/jgex && \
51+
echo "test -d \$JGEX_WD || (mkdir -p \$JGEX_WD; cd \$SNAP/root; cp -a -u * \$JGEX_WD)" >> ../install/bin/jgex && \
52+
echo "cd \$JGEX_WD" >> ../install/bin/jgex && \
53+
echo "java -cp \$SNAP/usr/share/jgex/\\* wprover.GExpert \$*" >> ../install/bin/jgex && \
54+
chmod 755 ../install/bin/jgex
5555
5656
stage-packages:
5757
- bash
@@ -72,3 +72,4 @@ parts:
7272
snapcraftctl prime
7373
rm -f usr/lib/jvm/java-11-openjdk-*/lib/security/blacklisted.certs
7474
rm -fr jar
75+

‎src/index.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
(async function () {
1212
await cheerpjInit({ version: 11 , enableDebug: true});
1313
cheerpjCreateDisplay(1400, 800);
14-
await cheerpjRunJar("/app/Java-Geometry-Expert-0.86.jar");
14+
await cheerpjRunJar("/app/Java-Geometry-Expert-0.87.jar");
1515
<!-- TODO: Change the version number by copying it from the Java source dynamically. -->
1616
})();
1717
</script>

‎src/main/java/wprover/PanelProve.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1669,7 +1669,7 @@ String setNode(Cond co) {
16691669
ret += ", tooltip = \" \""; // do not show any tooltip
16701670
}
16711671
// The files Rule??.jpg are located in the folder web:
1672-
String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/docs/web/Rule" + rule + ".jpg?raw=true";
1672+
String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/main/resources/docs/web/Rule" + rule + ".jpg?raw=true";
16731673
ret += ", style = \"" + s + "\", shape = " + f + ", fillcolor = \"" + c + "\"" +
16741674
", URL=\"" + url + "\""
16751675
+ "];\n";
@@ -1702,7 +1702,7 @@ Node graphvizNode(Cond co) {
17021702
// For some reason, this does not work, we get
17031703
// an error org.apache.batik.dom.util.SAXIOException: Invalid byte 1 of 1-byte UTF-8 sequence.
17041704
// FIXME.
1705-
// String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/docs/web/Rule" + rule + ".jpg?raw=true";
1705+
// String url = "https://github.com/kovzol/Java-Geometry-Expert/blob/master/src/main/resources/docs/web/Rule" + rule + ".jpg?raw=true";
17061706
n = Node.builder().shape(s).table(table().border(0).bgColor(c).
17071707
cellBorder(0).cellSpacing(0).cellPadding(6).href(url).tooltip(tooltipstring).
17081708
tr(td().color(c).text(co.getNo() + ") " + co.getText())).

‎src/main/java/wprover/Version.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
*/
77
public class Version {
88

9-
private static String sversion = "0.86";
9+
private static String sversion = "0.87";
1010
private static String data = "2024-11-26";
1111
private static String project = "Geometry Expert";
1212

‎src/test/import-ggb-prove-gdd-export-gv-png‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
#!/bin/bash
2-
# This script runs all .ggb files from ../docs/import/ggb-benchmarks,
3-
# proves them via the GDD method and saves the proof tree as .gv and .png in ../docs.
2+
# This script runs all .ggb files from ../main/resources/docs/import/ggb-benchmarks,
3+
# proves them via the GDD method and saves the proof tree as .gv and .png in ../main/resources/docs.
44

55
# Run this script with
66
# xvfb-run -a -s "-screen 0 1280x800x24" ./import-ggb-prove-gdd-export-gv-png
@@ -11,7 +11,7 @@
1111
# "snap" uses the snapcraft installation and considered therefore faster.
1212

1313

14-
BENCHMARKS_FOLDER=../docs/import/ggb-benchmarks # this may be changed on demand
14+
BENCHMARKS_FOLDER=../main/resources/docs/import/ggb-benchmarks # this may be changed on demand
1515
TIMEOUT=5 # JGEX forgets to quit sometimes, this timeout ensures proper exit
1616

1717
test -x $BENCHMARKS_FOLDER || {
@@ -61,21 +61,21 @@ for FULLNAME in `find $BENCHMARKS_FOLDER -name '*.ggb' | sort`; do
6161
GV=$GV_DIR/$NAME.gv
6262
rm -f $GV # remove a possible successful export from a previous run
6363
if [ "$1" = "snap" ]; then
64-
/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
64+
/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
6565
else
6666
pushd ../.. >/dev/null
6767
RUNTIME=`pwd`/build/install/jgex/bin/Java-Geometry-Expert
68-
/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
68+
/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
6969
popd >/dev/null
7070
fi
71-
PROBLEM=`cat ../docs/$NAME.log | grep "Unimplemented\|Unidentified\|Unsupported\|Exception" | grep -v "org.graphper.draw.ExecuteException" | head -1`
71+
PROBLEM=`cat ../main/resources/docs/$NAME.log | grep "Unimplemented\|Unidentified\|Unsupported\|Exception" | grep -v "org.graphper.draw.ExecuteException" | head -1`
7272
test -s $GV && {
7373
MD5SUM=`md5sum $GV | cut -f1 -d" "`
7474
if [ "$MD5SUM" = "d872444bcef19cb5462bb9a4fb4e9fb3" -o "$MD5SUM" = "3c964068bf7b811e7570449adc59af0e" -o "$MD5SUM" = "dd5ece2abd55b6f9b27df4df90e66fdf" ]; then
7575
echo -e "$WARNING_COLOR$NAME unsuccessful: empty gv tree, $PROBLEM$RESUME_COLOR"
7676
BAD=$((BAD+1))
7777
else
78-
dot -Tpng $GV > ../docs/$NAME.png
78+
dot -Tpng $GV > ../main/resources/docs/$NAME.png
7979
LENGTH=`cat $GV | wc -l`
8080
echo -e "$CORRECT_COLOR$NAME successful: $LENGTH lines of gv output$RESUME_COLOR"
8181
GOOD=$((GOOD+1))

‎src/test/prove-gdd-export-gv-svg‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
#!/bin/bash
2-
# This script runs all .gex files from ../docs/examples/6_GDD_FULL,
3-
# proves them via the GDD method and saves the proof tree as .gv and .svg in ../docs.
2+
# This script runs all .gex files from ../main/resources/docs/examples/6_GDD_FULL,
3+
# proves them via the GDD method and saves the proof tree as .gv and .svg in ../main/resources/docs.
44

55
# Run this script with
66
# xvfb-run -a -s "-screen 0 1280x800x24" ./prove-gdd-export-gv-svg
@@ -14,8 +14,8 @@ cd ../..
1414
RUNTIME=`pwd`/build/install/jgex/bin/Java-Geometry-Expert
1515
MYDIR=`pwd`
1616

17-
for FULLNAME in `find src/docs/examples/6_GDD_FULL -name '*.gex' `; do
17+
for FULLNAME in `find src/main/resources/docs/examples/6_GDD_FULL -name '*.gex' `; do
1818
NAME=`basename $FULLNAME .gex`
19-
/bin/time -o src/docs/$NAME.txt /usr/bin/timeout -k $TIMEOUT $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME
20-
dot -Tsvg $NAME.gv > src/docs/$NAME.svg
19+
/bin/time -o src/main/resources/docs/$NAME.txt /usr/bin/timeout -k $TIMEOUT $TIMEOUT $RUNTIME -p gdd -o $NAME.gv -x $MYDIR/$FULLNAME
20+
dot -Tsvg $NAME.gv > src/main/resources/docs/$NAME.svg
2121
done

0 commit comments

Comments
 (0)