[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Interpreting of "ん" as "±" (or something else?)



Also, I should point out that the error is coming from SBCL.

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

> On Jul 11, 2015, at 7:55 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
> ▶ locale
> LANG="en_US.UTF-8"
> LC_COLLATE="en_US.UTF-8"
> LC_CTYPE="en_US.UTF-8"
> LC_MESSAGES="en_US.UTF-8"
> LC_MONETARY="en_US.UTF-8"
> LC_NUMERIC="en_US.UTF-8"
> LC_TIME="en_US.UTF-8"
> LC_ALL=
> 
> The results seem identical. I should probably point out that I’m using `zsh` instead of `bash` if that makes a difference.
> 
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> 
> 
> 
> 
>> On Jul 11, 2015, at 7:54 AM, Sam Owre <owre@xxxxxxxxxxx> wrote:
>> 
>> Hi Ben,
>> 
>> 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.
>> 
>> Thanks,
>> Sam
>> 
>> LANG=en_US.UTF-8
>> LC_COLLATE="en_US.UTF-8"
>> LC_CTYPE="en_US.UTF-8"
>> LC_MESSAGES="en_US.UTF-8"
>> LC_MONETARY="en_US.UTF-8"
>> LC_NUMERIC="en_US.UTF-8"
>> LC_TIME="en_US.UTF-8"
>> LC_ALL=
>> 
>> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
>> 
>>> I’m running on Mac OS X (Yosemite).
>>> 
>>> Best Regards,
>>> Ben Hocking
>>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>>> 
>>> 
>>> 
>>> 
>>>> 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>
>>>>> 
>