Menu
▾
▴
Re: [CZT-Devel] CZT Tool Install and execute from c++
|
From: Leo F. <leo...@ne...> - 2011-10-10 13:49:25
|
Urmas, Petra's problem was at parser-zeves, yet yours is at typechecker-zeves. So, they are not related (e.g., and if you get to typechecker-zeves you have already passed parser-zeves). Petra's problem is indeed an error, and has just been fixed. Yours, I am still unsure whether it's something for us or for you to do (e.g., problems with your Maven). The "-Dmaven.test.skip=true" isn't relevant, I think. It just switches testing off - which is bad in your case. Could you execute "mvn -e clean install >> issues.txt" and send me the output + issues.txt please? Best, Leo On 10 Oct 2011, at 13:26, Urmas Repinski wrote: Hello, Petra, Leo. I have an error during installation process. Some files are missed or cannot be downloaded. Could not find artifact net.sourceforge.czt:parser-zeves:jar:tests:1.6-SNAPSHOT Tests are absent in the SVN i think. for CZT Z/Eves (proofs) Typechecker. By the way, execution of this tests can be switched off using -Dmaven.test.skip=true option: mvn -Dmaven.test.skip=true clean install -rf :typechecker-zeves But they still should be downloaded otherwise the installation error appears. Hope this helped, Urmas. > Date: Tue, 11 Oct 2011 00:02:50 +1300 > From: Pet...@ec...<mailto:Pet...@ec...> > To: czt...@li...<mailto:czt...@li...> > Subject: Re: [CZT-Devel] CZT Tool Install and execute from c++ > > 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...<mailto: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...<mailto:CZT...@li...> > https://lists.sourceforge.net/lists/listinfo/czt-devel <ATT00001..txt><ATT00002..txt> |
