Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

A warning about missing pandoc-tangle causes spurious errors #95

Closed
pirapira opened this issue Sep 28, 2017 · 8 comments
Closed

A warning about missing pandoc-tangle causes spurious errors #95

pirapira opened this issue Sep 28, 2017 · 8 comments

Comments

@pirapira
Copy link
Contributor

On version: 9f848a6

$ ./tests/ci/with-k uiuck ./Build tests quick

yields the following exception:

== running: tests/proofs/hkg/approve-spec.k
WARNING: pandoc-tangle not installed. Ignoring changes in markdown files

java.lang.UnsupportedOperationException: missing SMTLib translation for .WordStack
        at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:483)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:550)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:550)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:550)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translateTerm(KILtoSMTLib.java:450)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:423)
        at org.kframework.backend.java.symbolic.ConjunctiveFormula.accept(ConjunctiveFormula.java:845)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)
        at org.kframework.backend.java.symbolic.KILtoSMTLib.translateImplication(KILtoSMTLib.java:189)
        at org.kframework.backend.java.symbolic.SMTOperations.impliesSMT(SMTOperations.java:59)
        at org.kframework.backend.java.symbolic.ConjunctiveFormula.impliesSMT(ConjunctiveFormula.java:760)
        at org.kframework.backend.java.symbolic.ConjunctiveFormula.implies(ConjunctiveFormula.java:704)
        at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:147)
        at org.kframework.backend.java.util.RewriteEngineUtils.lambda$evaluateConditions$0(RewriteEngineUtils.java:185)
        at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
        at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1374)
        at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
        at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
        at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
        at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
        at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
        at org.kframework.backend.java.util.RewriteEngineUtils.evaluateConditions(RewriteEngineUtils.java:187)
        at org.kframework.backend.java.symbolic.PatternMatcher.match(PatternMatcher.java:118)
        at org.kframework.backend.java.kil.KItem$KItemOperations.evaluateFunction(KItem.java:458)
        at org.kframework.backend.java.kil.KItem$KItemOperations.resolveFunctionAndAnywhere(KItem.java:331)
        at org.kframework.backend.java.kil.KItem.resolveFunctionAndAnywhere(KItem.java:279)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:104)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:271)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:112)
        at org.kframework.backend.java.kil.KList.accept(KList.java:152)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:178)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:271)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:112)
        at org.kframework.backend.java.kil.KList.accept(KList.java:152)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:178)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:271)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:112)
        at org.kframework.backend.java.kil.KList.accept(KList.java:152)
        at org.kframework.backend.java.symbolic.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:178)
        at org.kframework.backend.java.symbolic.SubstituteAndEvaluateTransformer.transform(SubstituteAndEvaluateTransformer.java:103)
        at org.kframework.backend.java.kil.KItem.accept(KItem.java:710)
        at org.kframework.backend.java.kil.Term.substituteAndEvaluate(Term.java:82)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:322)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:342)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:342)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.buildRHS(SymbolicRewriter.java:342)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:189)
        at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:642)
        at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.lambda$prove$3(InitializeRewriter.java:210)
        at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
        at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
        at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1374)
        at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
        at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
        at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:708)
        at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
        at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:499)
        at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.prove(InitializeRewriter.java:213)
        at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:161)
        at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:52)
        at org.kframework.krun.KRun.run(KRun.java:104)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:67)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
        at org.kframework.main.Main.runApplication(Main.java:415)
        at org.kframework.main.Main.runApplication(Main.java:264)
        at org.kframework.main.Main.main(Main.java:73)
<same exception repeated multiple times>
--- expected
+++ actual
@@ -1 +1,3 @@
+WARNING: pandoc-tangle not installed. Ignoring changes in markdown files
+
 true
== failure: tests/proofs/hkg/approve-spec.k
== failed: 1 / 5

which might be and might not be related to the absense of pandoc-tangle.
@pirapira
Copy link
Contributor Author 

$ java -version
java version "1.8.0_144"
Java(TM) SE Runtime Environment (build 1.8.0_144-b01)
Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed mode)

@ehildenb
Copy link
Member

Confirmed (though the test is passing, there is an enormous amount of output).

Better to reproduce with ./tests/ci/with-k uiuck ./Build test tests/proofs/hkg/approve-spec.k (because ./Build tests quick selects tests randomly).

The enormous amount of output is more an issue directly with K, I'll open an issue there so we can start getting more informative messages out of K when proofs aren't going perfectly.

@ehildenb
Copy link
Member

And your intuition is correct that pandoc-tangle missing is not causing this issue, though that may be why the test reports as failed when on a system with pandoc-tangle it will report as passed. I'll investigate that too. The repository https://github.com/ehildenb/pandoc-tangle has a Linux binary for pandoc-tangle. I can see about getting a MacOS binary in there too if you need that.

@ehildenb ehildenb mentioned this issue Sep 28, 2017
Open
@ehildenb
Copy link
Member

Confirmed that when pandoc-tangle binary is not present, reports test failure even though test passes because the message === WARNING: pandoc-tangle not installed ... is being interpreted as output and compared to the value true, which is the expected output.

@pirapira
Copy link
Contributor Author

Then this issue is more like "warning about missing pandoc-tangle causes spurious errors." I'll change the title.

@pirapira pirapira changed the title ./Build tests quick without pandoc-tangle yields Java exceptions A warning about missing pandoc-tangle causes spurious errors Sep 28, 2017
@ehildenb
Copy link
Member

On branch quieter-proofs, you should be able to (replace bash with your preferred shell)

./tests/ci/with-k uiuck bash
./Build tests proofs approve-spec

It will output all the K warnings still, but should now say passed instead of failed.

I'll wait to turn this into a PR until we have K being quieter about the translation issues, and bump the submodule version when that happens.

@pirapira
Copy link
Contributor Author

@ehildenb I can confirm the behavior on quieter-proofs.

@pirapira
Copy link
Contributor Author

This issue has disappeared.

rv-jenkins added a commit that referenced this issue May 5, 2020
@rv-jenkins
deps/plugin: 42d31c1 - Remove obsolete files (#95)
9cc6e8b
rv-jenkins added a commit that referenced this issue May 5, 2020
@rv-jenkins @ehildenb
Update dependency: deps/plugin (#789)
a6a1823 
* deps/plugin: 42d31c1 - Remove obsolete files (#95)

* cmake/client: adjust for new location of init files

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@pirapira @ehildenb