From: Jon L. <ja...@bu...> - 2012-07-29 21:02:42
|
Andrius, I checked my permissions and I have been trying to work with the file, and I have no permissions on the file set that would prevent me from deleting it while the code is compiled. I am the admin on my machine and have also tried running the compilation in admin mode, to no success. It is also in a folder that allows for complete modification and removal of files. Is there any possibility that you may have some permissions set on the file when you were working on the repository? Thanks, Jon Lockhart On Mon, Jul 23, 2012 at 2:00 PM, Andrius Velykis <an...@ve...> wrote: > Dear Jon, > > It says it cannot delete the following test file: > C:\Users\Jon\MyCZT\czt\vcg\target\test-classes\tests\z\zstateref_ref.tex > > Do you have it open in some editor? Or does it have some bad permissions? > > Best regards, > ~Andrius > > On 23 Jul 2012, at 18:44, Jon Lockhart wrote: > > > Dear Leo, > > > > Thanks for the information you provided. After some digging into the > install more, I noticed what you mentioned and that the installer is just > throwing an exception on these particular sets of tests and is printing > them to the terminal. On closer examination the runs do return that all 25 > have succeeded successfully. > > > > As per your question, I am currently exploring the space of tool sets > that are available currently for Zed to help me write and prove > specifications that I am writing. I am currently developing some and > exploring Zed as a possible avenue for my dissertation. > > > > Dear Andrius, > > > > I was interested in what Leo said so I ran an install again, and he was > right in that the output was just from an exception thrown and not actually > causing an error. Since I started running the tests again I have come > across the same error ever time in VCG which causes it to fail compiling. > It appears to be in the zstarteref tests for VCG which reports that it had > 123 runs and 1 failure. > > > > Attached is the screen shot of the end of the install, along with the > surefire reports on this test from VCG. > > > > Thanks, > > Jon Lockhart > > > > On Mon, Jul 23, 2012 at 4:12 AM, Leo Freitas < > leo...@ne...> wrote: > > Hi guys, > > > > Perhaps I could she some light to this regarding the VCG... > > > > Within the test files I've added, there are some that are known to fail, > yet are not implemented / fixed. > > Those appear in (a verbose) output as a reminder of the fact, as well as > a warning to what is not implemented. > > Many of these cases have to do with weird uses of the schema calculus > allowed by the standard. Ex: > > > > \begin{axdef} > > S == [ x: \nat | P(x) ] \\ > > \end{axdef} > > > > (i.e. const declarations as part of an axiomatic box declPart; and other > similar cases within other declParts). > > I call this "weird" because it does not aggregate much expressiveness > value (i.e. you can say the same thing > > in other clearer ways) yet make tool building a nightmare! (e.g. see > Andrew Martin's paper > http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.7231). > > > > Another category is to do with name collusion, which could happen in > practice, although not as often: > > > > S == [ x: \power(\nat \cross \nat) | P(x) ] > > T == [ x: \num \pfun \nat | Q(x) ] > > R == [ x: \seq (0 \upto 20) | M(x) ] > > Op == S \land T \land R > > > > In this case, you have "x" with three different declared type, yet they > are type-compatible: the function and the > > sequence types used are indeed sets of pairs of numbers (i.e. > typechecking in Z is maximal, hence the greatest-common-type > > is used in order to enable automatic typechecking; otherwise one would > have a situation that to typecheck a Z specificaiton you > > would need to prove as many theorems as typechecking conditions.). So, > in effect, Op equals to: > > > > Op == [ x: \power(\arithmos \cross \arithmos) | P(x) \land Q(x) \land > R(x) \land x \in \power(\nat \cross \nat) \cap (\num \pfun \nat) \cap (\seq > (0 \upto 20)) ] > > > > When creating VCs, the VCG has a (strict) setting of typechecking its > generated VCs. Trouble is that in certain scenarios of complicated > > uses of the schema calculus not yet implemented by the VCG, the VCs > might not typecheck (if the solution is easily enough fixable by a user), > > hence the error. The test harness has a series of cases where such > unhandled examples exist. > > > > In any case, there shouldn't be an error in the final Mavan test report, > despite the verbose output. From your latest files, it says > > > > > ------------------------------------------------------------------------------- > > Test set: net.sourceforge.czt.vcg.util.DefinitionTableTest > > > ------------------------------------------------------------------------------- > > Tests run: 25, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 1.237 > sec > > > > which tells there were no errors from that run. > > > > I agree this is not ideal - I will try an fix that by having flags to > the build process so that verbosity is hidden from the user. > > > > For the extra needed implementation features to cover more of the schema > calculus, the solution is not straightforward, as ultimately, > > one would need full schema normalisation, which is quite tricky to > achieve (i.e. see the Rules project for more on this). In practice, > > I took a pragmatic approach: I implement the bits that I needed for the > examples I handled. Given the driving example(s) already contained > > quite complicated Z schema calculus usage (i.e. Mondex smartcards and > Tokeneer ID station, etc), I am going to add more as needed. > > For instance, another case where the VCG could generate a > type-incorrect-due-to-schema-calculus-issues (if the VC one needs) is when > > certain uses of generic types appear in the schemas used. > > > > In any case, thank you very much for your input and for the interest in > CZT. > > > > By the way, could I ask what do you have in mind with using CZT? Would > you be interested in implementation of features / ideas? > > > > Many thanks again, > > > > Best, > > Leo > > > > On 22 Jul 2012, at 23:01, Jon Lockhart wrote: > > > >> Dear Andrius, > >> > >> Just tried installing on my desktop. Everything was running great and a > lot faster on my Win 7 box, but I hit another error while installing, this > time on VCG. It says that there was an exception thrown when running the > one of the test that has tables in it. > >> > >> As always I have included the Surefire reports for you to look at. > >> > >> Thanks, > >> Jon > >> > >> > >> On Fri, Jul 20, 2012 at 1:39 PM, Andrius Velykis <an...@ve...> > wrote: > >> Dear Jon, > >> > >> It is possible that you just physically run out - the settings > -Xmx1024m say that you allocate Maven 1 gig of RAM (1024 megabytes). Please > try it on your desktop - hope the error goes away. > >> > >> Best regards, > >> ~Andrius > >> > >> > >> > >> On 20 Jul 2012, at 17:17, Jon Lockhart wrote: > >> > >> > Dear Andrius, > >> > > >> > I realize I only have a gig of ram on this really old laptop I am > using for developments and things of that nature. Its convenient for taking > to the lab and back, but I realize now it may not be enough and I may have > to switch to my desktop if that is the case. > >> > > >> > When the build quits on the error saying Java has run out of space, > it says that it is the Java Heap, not PermGen or anything else that is out > of space. > >> > > >> > Thanks, > >> > Jon Lockhart > >> > > >> > On Fri, Jul 20, 2012 at 2:31 AM, Andrius Velykis <an...@ve...> > wrote: > >> > Dear Jon, > >> > > >> > Good to hear about the fixes. > >> > > >> > Interesting out of memory issues - I am pretty sure 1024 and 512 are > >> > enough. Could you show the exact error message? Is it Heap Space or > >> > PermGen or other? > >> > > >> > How much actual memory do you have on your machine? > >> > > >> > Best regards, > >> > ~Andrius > >> > > >> > On Fri, Jul 20, 2012 at 2:41 AM, Jon Lockhart <ja...@bu...> > wrote: > >> > > Dear Andrius, > >> > > > >> > > Those fixes have seemed to help just fine, and I get well beyond > them now > >> > > when installing. > >> > > > >> > > Now I get an issue when installing the JFlex package. It says I am > out of > >> > > memory and I need to increase the heap size. I had my variables set > for > >> > > Maven to 1024 and 512, just like the INSTALL.md said to do and then > I bumped > >> > > them up to 2048 and 1024 respectively, and that also did not seem > to help. > >> > > > >> > > Any suggestions on this error? I don't think I want to increase the > Java > >> > > space too much more. > >> > > > >> > > Thanks, > >> > > Jon Lockhart > >> > > > >> > > > >> > > On Thu, Jul 19, 2012 at 4:18 PM, Andrius Velykis < > an...@ve...> wrote: > >> > >> > >> > >> Dear Jon Lochart, > >> > >> > >> > >> I guess we have to congratulate you again - you found another bug > >> > >> (filed as #3546060: > >> > >> > >> > >> > https://sourceforge.net/tracker/index.php?func=detail&aid=3546060&group_id=86250&atid=578942 > ). > >> > >> > >> > >> What is _extremely_ suprising that you are the first one to have > >> > >> stumbled on it. The issue is that there were problems with handling > >> > >> paths that have spaces in them (e.g. your "Documents and > Settings"). > >> > >> The exceptions appear every time you put the CZT repository on a > path > >> > >> with spaces. Surprisingly, no-one has ever done it! :) > >> > >> > >> > >> So thanks for the report - I have fixed it in the Git repository. > >> > >> Please update and re-run the Maven build. > >> > >> > >> > >> ~Andrius > >> > >> > >> > >> On Thu, Jul 19, 2012 at 7:16 PM, Jon Lockhart <ja...@bu...> > wrote: > >> > >> > Dear Leo Freitas, > >> > >> > > >> > >> > I apologize about that. Andrius asked about that before and it > looks > >> > >> > like I > >> > >> > forgot to reply to the developer list. > >> > >> > > >> > >> > I am running Windows XP Professional, Service Pack 3, 32-bit. > >> > >> > > >> > >> > I am currently not using an IDE with this software but was > hoping to get > >> > >> > it > >> > >> > compiled and installed to operate in either Eclipse or jEdit. > >> > >> > > >> > >> > > >> > >> > Dear Andrius Velykis, > >> > >> > > >> > >> > I reset my variable to be true as you prescribed and then tried > the hard > >> > >> > reset of CZT folder, but I still ran into the same error as > before. > >> > >> > > >> > >> > I then proceeded to do a fresh checkout of the git repository > and that > >> > >> > installed just fine for SpecReader. > >> > >> > > >> > >> > Unfortunately now I run into a new problem. When Typechecker is > being > >> > >> > tested, the first test, which is TypeCheckerTest, an error > occurs in > >> > >> > testing, rather than a failure, but of course this causes the > build to > >> > >> > fail. > >> > >> > > >> > >> > I have included attached to this email a screen shot of the last > lines > >> > >> > as > >> > >> > like before, and I included the xml and txt files from the > surefire > >> > >> > reports. > >> > >> > > >> > >> > > >> > >> > Thanks, > >> > >> > Jon Lockhart > >> > >> > > >> > >> > > >> > >> > > >> > >> > On Thu, Jul 19, 2012 at 12:31 PM, Andrius Velykis < > an...@ve...> > >> > >> > wrote: > >> > >> >> > >> > >> >> Dear Jon Lockhart, > >> > >> >> > >> > >> >> Thanks for spotting the problem. We were not handling the > Windows line > >> > >> >> breaks correctly. It seems that the Specreader module was > expecting to > >> > >> >> be working with Unix-style line breaks (see bug #3545808 for > details: > >> > >> >> > >> > >> >> > >> > >> >> > https://sourceforge.net/tracker/?func=detail&aid=3545808&group_id=86250&atid=578942 > ). > >> > >> >> > >> > >> >> I have committed a workaround which allows tests to go through > for > >> > >> >> now. As a result of this, I have also committed better handling > of > >> > >> >> line breaks when checking out/committing to our Git repository. > We are > >> > >> >> now expecting to have Windows style line breaks on Windows. > >> > >> >> > >> > >> >> To get the build working, you need to set the conversion to > >> > >> >> Windows-style line breaks back to original: > >> > >> >> > >> > >> >> git config --global core.autocrlf true > >> > >> >> > >> > >> >> Then you need to reset your Git repository (execute the > following > >> > >> >> commands in the root of your CZT checkout): > >> > >> >> > >> > >> >> del .git\index > >> > >> >> git reset --hard > >> > >> >> > >> > >> >> Alternatively, you could re-checkout the CZT repository from > Git. > >> > >> >> > >> > >> >> Now the Maven build should go through. I tested it on my > Windows 7 > >> > >> >> machine. > >> > >> >> > >> > >> >> Could you report your results? > >> > >> >> > >> > >> >> Thanks! > >> > >> >> ~Andrius > >> > >> >> > >> > >> >> On Thu, Jul 19, 2012 at 8:28 AM, Leo Freitas > >> > >> >> <leo...@ne...> wrote: > >> > >> >> > Hi Jon, > >> > >> >> > > >> > >> >> > This is indeed a puzzling error... in the past I encountered > such > >> > >> >> > character encoding errors when using variations of Eclipse and > >> > >> >> > Netbeans IDEs > >> > >> >> > and the > >> > >> >> > problem was associated to the way their character encoding > was setup > >> > >> >> > due > >> > >> >> > to, within my Windows environment, me having Portuguese and > English > >> > >> >> > as > >> > >> >> > languages with input (i.e. Netbeans v5 i think, thought it > useful to > >> > >> >> > change the character encoding of one test file because it > somehow > >> > >> >> > figured > >> > >> >> > out it was for > >> > >> >> > Portuguese encoding, despite the fact I haven't asked for this > >> > >> >> > neither > >> > >> >> > used Portuguese there!). > >> > >> >> > > >> > >> >> > We will try rebuilding it under windows here to see if it > happens for > >> > >> >> > us > >> > >> >> > --- otherwise, we would need to know more about your local > >> > >> >> > configuration > >> > >> >> > both IDE and OS I guess... > >> > >> >> > > >> > >> >> > Best, > >> > >> >> > Leo > >> > >> >> > > >> > >> >> > On 18 Jul 2012, at 22:06, Andrius Velykis wrote: > >> > >> >> > > >> > >> >> >> Dear Jon Lockhart, > >> > >> >> >> > >> > >> >> >> This looks like a very puzzling error - from the output it > seems > >> > >> >> >> that > >> > >> >> >> some characters are out of place (e.g. shifted in place). > Could you > >> > >> >> >> give a > >> > >> >> >> bit more information on your system? E.g. is it 32bit or > 64bit > >> > >> >> >> windows? What > >> > >> >> >> is your system character encoding? Which version of Java JDK > are you > >> > >> >> >> using? > >> > >> >> >> > >> > >> >> >> Thanks! > >> > >> >> >> > >> > >> >> >> Best regards, > >> > >> >> >> ~Andrius Velykis > >> > >> >> >> > >> > >> >> >> On 18 Jul 2012, at 20:59, Jon Lockhart wrote: > >> > >> >> >> > >> > >> >> >>> Dear Andrius Velykis, > >> > >> >> >>> > >> > >> >> >>> Thanks for all the suggestions and help. I used the > INSTALL.md file > >> > >> >> >>> this time and made some minor adjustments, like to my Maven > Java > >> > >> >> >>> variables, > >> > >> >> >>> but I still ran into the same test failures under installing > >> > >> >> >>> specreader. I > >> > >> >> >>> have attached the surefire txt and xml files to this email > along > >> > >> >> >>> with a > >> > >> >> >>> screen cap of the final lines of output that is given from > the > >> > >> >> >>> Maven build. > >> > >> >> >>> > >> > >> >> >>> I hope it will help in figuring out how alleviate the > problems I am > >> > >> >> >>> having with the install. I have tried everything I can > think of to > >> > >> >> >>> get past > >> > >> >> >>> these errors. > >> > >> >> >>> > >> > >> >> >>> Thanks > >> > >> >> >>> Jon Lockhart > >> > >> >> >>> > >> > >> >> >>> On Wed, Jul 18, 2012 at 5:34 AM, Andrius Velykis > >> > >> >> >>> <an...@ve...> > >> > >> >> >>> wrote: > >> > >> >> >>> Dear Jon Lockhart, > >> > >> >> >>> > >> > >> >> >>> Thanks for reporting your experiences building CZT. Could > you send > >> > >> >> >>> more details about the error that is occurring for you? The > last > >> > >> >> >>> bits > >> > >> >> >>> of Maven build output would be good, or if tests are > failing, try > >> > >> >> >>> attaching surefire test reports with the failures. > >> > >> >> >>> > >> > >> >> >>> Also, there have been some changes since the last release, > so the > >> > >> >> >>> installation instructions on the website may not be fully > >> > >> >> >>> up-to-date. > >> > >> >> >>> > >> > >> >> >>> The SVN repository is no longer updated (currently > read-only and > >> > >> >> >>> will > >> > >> >> >>> be removed soon). All new code goes to the Git repository. > There > >> > >> >> >>> are > >> > >> >> >>> more up-to-date instructions on building CZT available in > the Git > >> > >> >> >>> repository: > >> > >> >> >>> > >> > >> >> >>> > http://czt.git.sourceforge.net/git/gitweb.cgi?p=czt/czt;a=blob_plain;f=INSTALL.md > >> > >> >> >>> > >> > >> >> >>> Finally, we have quite nice Eclipse plug-ins in the latest > version > >> > >> >> >>> for > >> > >> >> >>> CZT as an alternative to jEdit - the update site is built > together > >> > >> >> >>> with the whole CZT. > >> > >> >> >>> > >> > >> >> >>> I am looking into setting up a continuous integration (CI) > system > >> > >> >> >>> for > >> > >> >> >>> CZT soon. Hopefully then we will have "nightly" downloads > and there > >> > >> >> >>> will be less need to build everything manually. > >> > >> >> >>> > >> > >> >> >>> Best regards, > >> > >> >> >>> ~Andrius Velykis > >> > >> >> >>> > >> > >> >> >>> > >> > >> >> >>> On Tue, Jul 17, 2012 at 9:00 PM, Jon Lockhart < > ja...@bu...> > >> > >> >> >>> wrote: > >> > >> >> >>>> Dear CZT Developers, > >> > >> >> >>>> > >> > >> >> >>>> I am having an issue building versions of the CZT tool set > in > >> > >> >> >>>> Windows, and I > >> > >> >> >>>> am wondering if anyone has had a similar issue recently or > in the > >> > >> >> >>>> past and > >> > >> >> >>>> has a suggestion for handling this problems, or a > solution, which > >> > >> >> >>>> would be > >> > >> >> >>>> more beneficial in my case. > >> > >> >> >>>> > >> > >> >> >>>> I first started with following the installation > instructions on > >> > >> >> >>>> the > >> > >> >> >>>> site, > >> > >> >> >>>> and downloaded an available copy of the svn version of > 1.5, git > >> > >> >> >>>> bash, > >> > >> >> >>>> maven, > >> > >> >> >>>> and jedit. While trying to build the czt files, after got > through > >> > >> >> >>>> all > >> > >> >> >>>> the > >> > >> >> >>>> installation instructions for the various tool sets, I ran > into a > >> > >> >> >>>> dependency > >> > >> >> >>>> error on typechecker. Now I know that in the install it > says that > >> > >> >> >>>> dependency > >> > >> >> >>>> errors will arise and that I just continue to try > reinstalling but > >> > >> >> >>>> after > >> > >> >> >>>> several attempts all resulting in the same error, I > decided that I > >> > >> >> >>>> should > >> > >> >> >>>> try getting the latest version of CZT from the git > repository, > >> > >> >> >>>> seeing > >> > >> >> >>>> that > >> > >> >> >>>> it was a newer version and maybe some of these dependency > errors > >> > >> >> >>>> would be > >> > >> >> >>>> resolved. Unfortunately this was not the case and in fact > I also > >> > >> >> >>>> ran > >> > >> >> >>>> into an > >> > >> >> >>>> error in one of the tests for typechecker. So this time > around I > >> > >> >> >>>> had > >> > >> >> >>>> a test > >> > >> >> >>>> error occur every time for type checker, and then I am > always > >> > >> >> >>>> running > >> > >> >> >>>> into > >> > >> >> >>>> the same dependency error with the rules with the latest > version > >> > >> >> >>>> from > >> > >> >> >>>> git. > >> > >> >> >>>> > >> > >> >> >>>> I have tried downloading version 1.5 and 1.6 again > multiple times > >> > >> >> >>>> thinking > >> > >> >> >>>> that there was possibly an error in the download I had, I > have > >> > >> >> >>>> tried > >> > >> >> >>>> increasing the java stack in my maven variables to 512 > from 256, > >> > >> >> >>>> and > >> > >> >> >>>> I have > >> > >> >> >>>> even tried looking through the mail repository to see if > anyone > >> > >> >> >>>> else > >> > >> >> >>>> has had > >> > >> >> >>>> an issue with compiling these more recent versions on > Windows, but > >> > >> >> >>>> I > >> > >> >> >>>> didn't > >> > >> >> >>>> see any. > >> > >> >> >>>> > >> > >> >> >>>> As I said I am very open to fixes, solutions, or a work > around for > >> > >> >> >>>> getting > >> > >> >> >>>> CZT compiled on a Windows box, so that I can import the > necessary > >> > >> >> >>>> jar > >> > >> >> >>>> files > >> > >> >> >>>> into jEdit so I can start using that for my writing of Zed > >> > >> >> >>>> specifications. > >> > >> >> >>>> > >> > >> >> >>>> Thanks, > >> > >> >> >>>> Jon Lockhart > >> > >> >> >>>> > >> > >> >> >>>> > >> > >> >> >>>> > >> > >> >> >>>> > ------------------------------------------------------------------------------ > >> > >> >> >>>> Live Security Virtual Conference > >> > >> >> >>>> Exclusive live event will cover all the ways today's > security and > >> > >> >> >>>> threat landscape has changed and how IT managers can > respond. > >> > >> >> >>>> Discussions > >> > >> >> >>>> will include endpoint security, mobile security and the > latest in > >> > >> >> >>>> malware > >> > >> >> >>>> threats. > http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > >> > >> >> >>>> _______________________________________________ > >> > >> >> >>>> CZT-Devel mailing list > >> > >> >> >>>> CZT...@li... > >> > >> >> >>>> https://lists.sourceforge.net/lists/listinfo/czt-devel > >> > >> >> >>>> > >> > >> >> >>> > >> > >> >> >>> > >> > >> >> >>> > >> > >> >> >>> > <net.sourceforge.czt.specreader.PermuteMarkupTest.txt><SpecReaderError.jpg><TEST-net.sourceforge.czt.specreader.PreludeTest.xml><net.sourceforge.czt.specreader.PreludeTest.txt><TEST-net.sourceforge.czt.specreader.PermuteMarkupTest.xml> > >> > >> >> >> > >> > >> >> >> > >> > >> >> >> > >> > >> >> >> > >> > >> >> >> > ------------------------------------------------------------------------------ > >> > >> >> >> Live Security Virtual Conference > >> > >> >> >> Exclusive live event will cover all the ways today's > security and > >> > >> >> >> threat landscape has changed and how IT managers can respond. > >> > >> >> >> Discussions > >> > >> >> >> will include endpoint security, mobile security and the > latest in > >> > >> >> >> malware > >> > >> >> >> threats. > http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > >> > >> >> >> _______________________________________________ > >> > >> >> >> CZT-Devel mailing list > >> > >> >> >> CZT...@li... > >> > >> >> >> https://lists.sourceforge.net/lists/listinfo/czt-devel > >> > >> >> > > >> > >> > > >> > >> > > >> > > > >> > > > >> > > >> > >> > >> > <net.sourceforge.czt.vcg.util.DefinitionTableTest.txt><TEST-net.sourceforge.czt.vcg.util.DefinitionTableTest.xml><CZT > - VCG - > Error.jpg>------------------------------------------------------------------------------ > >> > >> Live Security Virtual Conference > >> Exclusive live event will cover all the ways today's security and > >> threat landscape has changed and how IT managers can respond. > Discussions > >> will include endpoint security, mobile security and the latest in > malware > >> threats. > http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/_______________________________________________ > >> CZT-Devel mailing list > >> CZT...@li... > >> https://lists.sourceforge.net/lists/listinfo/czt-devel > > > > > > <net.sourceforge.czt.vcg.z.refinement.RefinementTest.txt><CZT - VCG - > Error.jpg><TEST-net.sourceforge.czt.vcg.z.refinement.RefinementTest.xml> > > |