Re: [tlaplus] building tlaplus from source fails

[owen...@xxxxxxxxx]

On Saturday, November 17, 2018 at 10:49:51 PM UTC-5, Markus Alexander Kuppe wrote:
> On 17.11.18 18:41, wrote:
> > Downloading the nightly builds would be a bit wasteful on my end, git pull is a lot simpler process.
> >
> > Even after a few days, the error still persists but that's an upstream issue.
> >
> > Skipping the tests with
> > mvn clean install -DskipTests
> >
> > successfully builds the project.
> >
> > How do I actually run the .jar files; I am getting cannot find main errors.
> 
> 
> Hi Owen,
> 
> without knowing exactly what you have tried, I can only point you to the
> zip files located in
> org.lamport.tla.toolbox.product.product/target/products/.  From there
> you can follow the regular Toolbox documentation.
> 
> Hope this helps,
> 
> Markus

After cloning the tlaplus github repo, git log:
commit 4605eac8e720ae54cba08522c1bc6890e74d2998 (HEAD -> master, origin/master, origin/HEAD)
Author: Markus Alexander Kuppe <tlapl...@xxxxxxxxxxx>
Date:   Sun Nov 11 16:50:47 2018 -0800

    Prevent div-by-zero in calculating collision probability when zero
    states are generated.
    
    [Bug][TLC]

i went to the root directory; ls
CONTRIBUTING.md
examples
general
keystore
LICENSE
org.lamport.tla.distributed.consumer
org.lamport.tla.toolbox
org.lamport.tla.toolbox.doc
org.lamport.tla.toolbox.editor.basic
org.lamport.tla.toolbox.feature.base
org.lamport.tla.toolbox.feature.branding
org.lamport.tla.toolbox.feature.editor
org.lamport.tla.toolbox.feature.help
org.lamport.tla.toolbox.feature.jclouds
org.lamport.tla.toolbox.feature.jnlp
org.lamport.tla.toolbox.feature.prover
org.lamport.tla.toolbox.feature.standalone
org.lamport.tla.toolbox.feature.tla2tex
org.lamport.tla.toolbox.feature.tlc
org.lamport.tla.toolbox.feature.uitest
org.lamport.tla.toolbox.jclouds
org.lamport.tla.toolbox.jnlp
org.lamport.tla.toolbox.p2repository
org.lamport.tla.toolbox.product.product
org.lamport.tla.toolbox.product.standalone
org.lamport.tla.toolbox.test
org.lamport.tla.toolbox.tool.prover
org.lamport.tla.toolbox.tool.tla2tex
org.lamport.tla.toolbox.tool.tla2tex.uitest
org.lamport.tla.toolbox.tool.tlc
org.lamport.tla.toolbox.tool.tlc.test
org.lamport.tla.toolbox.tool.tlc.ui
org.lamport.tla.toolbox.tool.tlc.ui.test
org.lamport.tla.toolbox.tool.tlc.ui.uitest
org.lamport.tla.toolbox.uitest
org.lamport.tlatools.api
org.lamport.tlatools.consumer.distributed
org.lamport.tlatools.feature
org.lamport.tlatools.impl.distributed
pom.xml
README.md
states
tlatools

I run mvn clean install -DskipTests
because the tests cause the build to fail.

After a while it mvn shows success
example folder: cd org.lamport.tla.toolbox/src/org/lamport/tla/toolbox
AbstractTLCActivator.java
Activator.java
job
OpenFileManager.java
spec
tool
ToolboxDirectoryVisitor.java
ui
util

there's also a .m2/repository directory in my home folder
antlr
aopalliance
asm
avalon-framework
backport-util-concurrent
classworlds
com
commons-beanutils
commons-chain
commons-cli
commons-codec
commons-collections
commons-digester
commons-httpclient
commons-io
commons-lang
commons-logging
commons-validator
de
dom4j
javax
junit
log4j
logkit
org
oro
p2
sslext
tlatoolbox
xerces
xml-apis
xmlunit

from: ~/.m2/repository/tlatoolbox/org.lamport.tla.toolbox/1.0.0-SNAPSHOT

java -jar org.lamport.tla.toolbox-1.0.0-SNAPSHOT.jar
no main manifest attribute, in org.lamport.tla.toolbox-1.0.0-SNAPSHOT.jar

java org.lamport.tla.toolbox-1.0.0-SNAPSHOT.jar 
Error: Could not find or load main class org.lamport.tla.toolbox-1.0.0-SNAPSHOT.jar