Re: [CZT-Devel] Issues Building CZT in Windows

[Leo F. <leo...@ne...>]

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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto: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...<mailto:CZT...@li...>
https://lists.sourceforge.net/lists/listinfo/czt-devel