[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Interpreting of "ん" as "±" (or something else?)
I just tried a fresh install of PVS 6.0 on Yosemite, with the same
results (no errors). Can you try typing 'locale' at a shell window?
You should get something like the following.
Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> I’m running on Mac OS X (Yosemite).
> Best Regards,
> Ben Hocking
> > On Jul 11, 2015, at 7:22 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> > Hi Ben,
> > What platform are you running on? I tried with and without patches on
> > Linux 64 bit, and it always typechecks under SBCL.
> > Thanks,
> > Sam
> > Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >> I cloned the NASA PVS Library and configured my environment to use it, but I still get that same
> >> problem. Does the solution possibly rely on the very latest PVS from GitHub as well?
> >> I am using 6.0, and have just cloned the PVS repository itself, as long as SBCL, but got stuck:
> >> • I did figure out that I needed to run autoconf
> >> • I also then figured out that my PVSPATH variable needs to end with a trailing “/“
> >> • building SBCL depended on having SBCL (or another LISP) already built
> >> I’ll eventually figure out how to build PVS, but just thought I’d let you know that with the default
> >> 6.0 PVS and the GitHub NASA libraries the problem persisted for me (on Mac OS X, if that’s relevant).
> >> Best Regards,
> >> Ben Hocking
> >> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >> On Jul 10, 2015, at 9:58 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:
> >> Ben,
> >> This theory type-checks without problem using the patches in the github
> >> version of the NASA PVS Library. Sam recently added the attached patch,
> >> which may have solved the problem.
> >> Cesar
> >> --
> >> Cesar A. Munoz NASA Langley Research Center
> >> Cesar.A.Munoz@xxxxxxxx Bldg. 1220 Room 115 MS. 130
> >> http://shemesh.larc.nasa.gov/people/cam Hampton, VA 23681-2199, USA
> >> Office: +1 (757) 864 1446 Fax: +1 (757) 864 4234
> >> On 7/10/15 3:31 AM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
> >> on behalf of Ben Hocking"
> >> <pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
> >> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >> exampleJapanese: THEORY
> >> BEGIN
> >> 真(p_しません: bool): bool =
> >> p_しません;
> >> しません(p_偽: bool): bool =
> >> NOT (p_偽);
> >> END exampleJapanese
> >> <patch-12.lisp>