Menu
▾
▴
Re: [CZT-Devel] CZT Tool Install and execute from c++
|
From: Leo F. <leo...@ne...> - 2011-10-10 11:39:45
|
Hi Petra, About the failure, from the numbers below I see it happened on ProofScriptParsingTest could you send me the name of the file on which it failed please? It's interesting the other user's failure was on typechecker and not the parser. Hum... --- About the debug log, yes, it's large.... They were added to enable easy pinpointing of tricky lexing errors when handling certain ZEves productions that are not quite within ISOz, and the fact we wanted all formats at the same level of stability, given there were various issues with extension for Unicode and XML printers (see SVN logs). The ZEves CZT parser is now stable, I will disable the debug flags. Thanks for pointing it out. The output is now quite silent: Running net.sourceforge.czt.parser.zeves.ScanningTest Tests run: 37, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.862 sec Running net.sourceforge.czt.parser.zeves.OnTheFlyParsingTest Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec Running net.sourceforge.czt.print.zeves.ZmlPrintTest Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec Running net.sourceforge.czt.parser.zeves.ProofScriptParsingTest Number of tests for Z/Eves proofs parsing: 41 Tests run: 41, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 9.121 sec Results : Tests run: 79, Failures: 0, Errors: 0, Skipped: 0 --- Best, Leo On 10 Oct 2011, at 12:02, Petra Dietrich wrote: > Hi there, > > I get the same error: > [INFO] CZT Z/Eves (proofs) Parser ........................ FAILURE > > due to a test failing: > Tests run: 41, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 29.787 > sec <<< FAILURE! > Running net.sourceforge.czt.print.zeves.ZmlPrintTest > Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec > > Results : > > Failed tests: > null(net.sourceforge.czt.parser.util.CztManagedTest$TestNormal) > Tests run: 79, Failures: 1, Errors: 0, Skipped: 0 > > BTW, it is hard to find useful output due to the huge amount of debug > output like: > ================================================================= > Direct UNICODE printing of > /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8 > > ============================ TOSTRING ============================ > toString successful for zeveslabels > > ================================================================== > SM UNICODE printing of > /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8 > > ============================ LATEX ============================ > created file > /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.tex > > ============================ XML ============================ > created file > /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.zml > ================================================================== > > Is there a way to switch that off? > > Cheers, > Petra > > On 10/10/11 23:20, Leo Freitas wrote: >> Hi Urmas, >> >> I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen. >> I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send >> us the maven detailed info? I think if you run "mvn -e clean install" it gives that. >> >> If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine). >> By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully. >> Could you please try again and let me know if you still get the problem? >> >> ---- >> >> About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator, >> which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types). >> >> How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code >> functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve? >> >> Best, >> Leo >> >> On 10 Oct 2011, at 10:41, Urmas Repinski wrote: >> >> Hello, >> >> I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++. >> >> First of all i want to install CZT on my PC. >> >> I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached >> >> [INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s] >> [INFO] CZT Z VCG ......................................... SKIPPED >> [INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED >> [INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED >> [INFO] CZT Z/Eves Integration ............................ SKIPPED >> .... >> >> >> So maybe i have to use any other mirror to download archives that are required during installation? >> I had tried all mirrors that are in MAVEN website - >> >> http://maven.apache.org/guides/mini/guide-mirror-settings.html >> >> But this does not solve the problem, the installation does not finish. >> >> And one more problem, can i after the installation animate simple Z specifications from c++ code? >> >> If yes then please somebody replay me how can i do that? >> >> Thank you very much, >> Urmas Repinski. >> <ATT00001..txt><ATT00002..txt> >> >> >> ------------------------------------------------------------------------------ >> All the data continuously generated in your IT infrastructure contains a >> definitive record of customers, application performance, security >> threats, fraudulent activity and more. Splunk takes this data and makes >> sense of it. Business sense. IT sense. Common sense. >> http://p.sf.net/sfu/splunk-d2dcopy1 >> _______________________________________________ >> CZT-Devel mailing list >> CZT...@li... >> https://lists.sourceforge.net/lists/listinfo/czt-devel > > > ------------------------------------------------------------------------------ > All the data continuously generated in your IT infrastructure contains a > definitive record of customers, application performance, security > threats, fraudulent activity and more. Splunk takes this data and makes > sense of it. Business sense. IT sense. Common sense. > http://p.sf.net/sfu/splunk-d2dcopy1 > _______________________________________________ > CZT-Devel mailing list > CZT...@li... > https://lists.sourceforge.net/lists/listinfo/czt-devel |
