Source Code

2/1/2020

It is the intention to 'open source' most, if not all, the source code used here. This will take some time to do, maybe a year or two.

The Deriver15 Application and Applet Source

https://github.com/mfricke1947/Deriver15Public

Deriver15.zip

#Deriver15Public

[Code compiles and runs with Eclipse 2019-09R (4.1.3.0) 1/31/2020]

Software for instruction in logic (as used on https://softoption.us ). 
This is the full source code for Deriver15, which is java code 
for displaying proofs, intelligent editing of derivations, tactics, 
drawing derivation trees, drawing semantic interpretations, symbolization 
etc. This code is pretty much unchanged since 2012. In 2015 the license 
notices were added, hence Deriver15.

The Java Build Path should have in it the source code and the JRE System 
Library, say Java SE 1.7 (although it won't be sensitive on that). It 
should also have JUnit 5 as a Library (as there is some JUnit test code).

The code can then be run within Eclipse as a Java Application with the main

   TDeriverApplication -- us.softoption.editor

The documentation on https://softoption.us would help here on what the 
application can do.

Eclipse can export the application as a Runnable JAR file, say Deriver15.jar.

It would be typical then to run this through Proguard, say 6.2.2 which will
obfuscate and compress it (from about 3.6 meg to 1 meg). It is important here
that the right configuration file be used for Proguard. Basically the 
consideration is that Java Beans are used to save to file, and this means
that when windows and contents are re-created from file the names of 
the classes cannot have been obfuscated. Some sample Proguard configuration 
files are included. Proguard may produce hundreds of warnings but yet run 
through successfully.

Then it would be usual to sign the compressed jar using jarsigner and Java 
key tool. It is possible to timestamp this.

Deriver15 has various 'switches' in it controlled through its preferences.
Sample logic instruction files are included.

The Deriver15 jar/application can be automatically downloaded and launched
using jnlp and Java Web Start. It also can configure itself when doing
this. Some sample files are included.

The source code for twenty or more applets is included. These used to be
embedded in web pages so as to have Deriver functionality without having
to have the application installed or downloaded. The applet code used to
be obfuscated, compressed, and signed.

This technology is dead. [Most of the applets have been rewritten as
javascript widgets, and that code is available elsewhere.]

However, you can still run the applets in Eclipse. The applets have
'applet' in their name somewhere. For example, us.softoption.gameApplets
has as one of its source files

   GamesQuiz.java

If you select that file and 'Run As Java Applet' Eclipse will do exactly 
that for you (and similarly for the other applets).


The Combinatory Logic Widget Source

https://github.com/mfricke1947/CombinatoryLogicPublic.git

CombinatoryLogic.zip

Software for instruction in logic (as used on http://softoption.us ). 
This is the source code for the Combinatory Logic Widget, which is 
some javascript for displaying proofs in combinatory logic. The Widget 
illustrates intelligent editing of derivations. The code is written 
in Java and the project hosted and developed in the Eclipse IDE 
Oxygen 3a), with GIT and the Google Web Toolkit (GWT 2.8.1) plug-in. 
The GWT plug-in can run the project in Super Dev mode for development. 
Then it compiles the Java to Javascript, which can be embedded in Web 
Pages (or ePubs, iBooks etc.). Various 'switches' in those Web Pages 
allow the Lambda Widget to be configured. Sample Web pages are included.
[Code compiles and runs with Eclipse and GWT 5/7/2018]

The Lambda Widget Source

https://github.com/mfricke1947/LambdaPublic.git

LambdaPublic.zip

Software for instruction in logic (as used on http://softoption.us ). 
This is the source code for the Lambda Widget, which is some javascript for 
displaying proofs in lambda calculus. The Widget illustrates intelligent 
editing of derivations, and tactics. The code is written in Java and the 
project hosted and developed in the Eclipse IDE (Oxygen 3a), with GIT and 
the Google Web Toolkit (GWT 2.8.1) plug-in. The GWT plug-in can run the 
project in Super Dev mode for development. Then it compiles the Java to 
Javascript, which can be embedded in Web Pages (or ePubs, iBooks etc.). 
Various 'switches' in those Web Pages allow the Lambda Widget to be configured. 
Sample Web pages are included.[Code compiles and runs with Eclipse and GWT 4/27/2018]

The Parsers Source

https://github.com/mfricke1947/ParserPublic.git

ParserPublic.zip

These are the parsers used for propositional and predicate logic on http://softoption.us . 
There are, possibly, four parsers. There are hand-written recursive descent 
parsers for the basic propositional and predicate logic, and for lambda calculus. 
Then there are two automatically generated parsers CCParser and CCParserTwo 
also for logic. All the actual parsers in use for the logic in the instructional 
software, and subclassed parsers all use CCParser or CCParserTwo. They can 
parse pretty well all the standard versions of logic (versions corresponding 
to all the standard textbooks). There is a single internal form, and the 
variations are translated into it when being read and parsed, then the 
formulas are written back in the desired flavor or style.

The Proof Widget Source

https://github.com/mfricke1947/ProofsPublic.git

ProofsPublic.zip

Software for instruction in logic (as used on http://softoption.us ). 
This is the source code for the Proof Widget, which is some javascript 
for displaying proofs in propositional logic, predicate logic, first-order 
theories, set theory, and lambda calculus. The Widget illustrates 
intelligent editing of derivations, tactics, and compiling derivations 
(best-path theorem proving). The code is written in Java and the 
project hosted and developed in the Eclipse IDE, with GIT and the 
Google Web Toolkit (GWT) plug-in. The GWT plug-in can run the project 
in Super Dev mode for development. Then it compiles the Java to 
Javascript, which can be embedded in Web Pages (or ePubs, iBooks etc.). 
Various 'switches' in those Web Pages allow the Proof Widget to be 
configured to run the desired systems. Sample Web pages are included.

The Trees Widget Source

https://github.com/mfricke1947/TreesJSPublic.git

TreesJSPublic.zip

Software for instruction in logic (as used on http://softoption.us ).
This is the source code for the Trees Widget, which is some javascript
for displaying trees in propositional logic, predicate logic, first-order theories,
modal logic, and set theory. The Widget illustrates extension and closing of tree.
The code is written in Java and the project hosted and
developed in the Eclipse IDE, with GIT and the Google Web Toolkit (GWT) plug-in. The
GWT plug-in can run the project in Super Dev mode for development. Then it compiles the
Java to Javascript, which can be embedded in Web Pages (or ePubs, iBooks etc.).
Various 'switches' in those Web Pages allow the Trees Widget to be configured to run
the desired systems. Sample Web pages are included. For these, go to TreesJS/war/
and then use a web browser on Tutorial1.html etc.