headers
Susanto Kong | 1 Aug 2008 05:25
Picon

Re: Q: installation MOSML

Hi Flemming,

Thank you for your input.
I am using Kubuntu 8.04 - 64bit (have to stick with 64).
I already followed peter's suggestion.
Basic MOSML build smoothly.
But not the dynamic links.
I have tried to build it one at a time.
So far I managed to build crypt, interface, mpg, mregex, and munix.
Failed on intinf, mgd, mgdbm, mmysql, and msocket.
I am not sure it is enough to build HOL.

Kong Susanto

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 4 comments |
headers
Michael Norrish | 1 Aug 2008 06:58
Picon
Favicon

Re: Q: installation MOSML

Susanto Kong wrote:
> Hi Flemming,
> 
> Thank you for your input.
> I am using Kubuntu 8.04 - 64bit (have to stick with 64).
> I already followed peter's suggestion.
> Basic MOSML build smoothly.
> But not the dynamic links.
> I have tried to build it one at a time.
> So far I managed to build crypt, interface, mpg, mregex, and munix.
> Failed on intinf, mgd, mgdbm, mmysql, and msocket.
> I am not sure it is enough to build HOL.

If you can build (and load) a dynamic library like munix, then you
have a good chance of being able to build all of HOL.  And the only
thing that the dynamic loading is needed for is HolBdd.  If you don't
need HolBdd, then you only need "basic" Moscow ML.

Michael.

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 3 comments |
headers
Mike Gordon | 1 Aug 2008 14:13
Picon
Picon
Favicon

Are timeouts possible in HOL (mosml or poly)?


Does anyone know if it is possible to run a function 
(e.g. SIMP_CONV arith_ss []) for a fixed time and then fail on
timeout. I vaguely remember that there was no way to do this, but
want to double check.

Mike

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 2 comments |
headers
Susanto Kong | 2 Aug 2008 02:55
Picon

Re: Q: installation MOSML

Thanks Michael,
After a bit tweaking, I managed to build HOL.
But with issues on muddy and smv.
Here is the warning & error output:

reorder.c: In function 'bdd_reorder_auto':
reorder.c:1629: warning: the address of 'bdd_reorder_ready' will
always evaluate as 'true'
ar: creating libbdd.a

In file included from grammar.y:2:
./storage.h:15: warning: conflicting types for built-in function 'malloc'
grammar.tab.c:462: error: conflicting types for 'malloc'
./storage.h:15: error: previous declaration of 'malloc' was here
grammar.y: In function 'yyparse':
grammar.y:284: warning: cast to pointer from integer of different size
make: *** [grammar.o] Error 1
Build failed in directory /home/kws/tools/hol/src/temporal/smv.2.4.3
(make failed).

I wonder what do you think about this message?

Kong Susanto

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
(Continue reading)

Permalink | Reply | 2 comments |
headers
freek | 2 Aug 2008 08:48
Picon
Favicon

Re: Are timeouts possible in HOL (mosml or poly)?

Dear Mike,

>Does anyone know if it is possible to run a function
>(e.g. SIMP_CONV arith_ss []) for a fixed time and then
>fail on timeout. I vaguely remember that there was no way
>to do this, but want to double check.

For my upcoming new Mizar mode for HOL Light I just implemented

  exception Timeout;;

  Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Timeout));;

  let TIMED_TAC n tac g =
    let _ = Unix.alarm n in
    try
      let gs = tac g in
      let _ = Unix.alarm 0 in
      gs
    with x ->
      let _ = Unix.alarm 0 in
      raise x;;

which seems to work well for me.  (Now that I look at this,
it really is generic and not related to tactics at all,
it really meaning "run this function on this argument for
n seconds".  Maybe I should rename it?)  So one can run

	TIMED_TAC 3 (SIMP_TAC[...])
(Continue reading)

Permalink | Reply | 0 comments |
headers
Makarius | 2 Aug 2008 13:19

Re: Are timeouts possible in HOL (mosml or poly)?

On Fri, 1 Aug 2008, Mike Gordon wrote:

> Does anyone know if it is possible to run a function (e.g. SIMP_CONV 
> arith_ss []) for a fixed time and then fail on timeout. I vaguely 
> remember that there was no way to do this, but want to double check.

This is reasonably easy in recent versions of Poly/ML (5.1 or 5.2), thanks 
to support for (native) Posix threads.  The basic idea is to have a 
watchdog interrupt the current worker after some time:

structure TimeLimit =
struct

exception TimeOut;

fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
  let
    val worker = Thread.self ();
    val timeout = ref false;
    val watchdog = Thread.fork (fn () =>
      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);

    (*RACE! timeout signal vs. external Interrupt*)
    val result = Exn.capture (restore_attributes f) x;
    val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);

    val _ = Thread.interrupt watchdog handle Thread _ => ();
  in if was_timeout then raise TimeOut else Exn.release result end) ();

end;
(Continue reading)

Permalink | Reply | 0 comments |
headers
Susanto Kong | 3 Aug 2008 13:32
Picon

Re: Q: installation MOSML

Thanks Hasan,
I made the update, seems it worked.
Kong Susanto

On Sun, Aug 3, 2008 at 9:26 AM, Hasan Amjad <ha227 <at> cam.ac.uk> wrote:
>
>
>>
>> reorder.c: In function 'bdd_reorder_auto':
>> reorder.c:1629: warning: the address of 'bdd_reorder_ready' will
>> always evaluate as 'true'
>> ar: creating libbdd.a
>>
>
> Looks like that source line should read
>
> if (!bdd_reorder_ready())
>
> rather than
>
> if (!bdd_reorder_ready)
>
> but, I am not a C hacker. You can ignore this warning unless you want to
> use MuDDy with dynamic reordering (it is disabled by default IIRC).
> Nothing in HOL/src uses MuDDy.
>
> Cheers,
> Hasan
>
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
Hasan Amjad | 3 Aug 2008 10:26
Picon
Picon
Favicon

Re: Q: installation MOSML


> 
> reorder.c: In function 'bdd_reorder_auto':
> reorder.c:1629: warning: the address of 'bdd_reorder_ready' will
> always evaluate as 'true'
> ar: creating libbdd.a
> 

Looks like that source line should read 

if (!bdd_reorder_ready())

rather than 

if (!bdd_reorder_ready)

but, I am not a C hacker. You can ignore this warning unless you want to
use MuDDy with dynamic reordering (it is disabled by default IIRC).
Nothing in HOL/src uses MuDDy.

Cheers,
Hasan 

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
Permalink | Reply | 1 comment |
headers
Otmane Ait Mohamed | 7 Aug 2008 01:14
Picon
Picon
Favicon

LAST CALL FOR PARTICIPATION (TPHOLs'2008)


                LAST CALL FOR PARTICIPATION

21st International Conference on Theorem Proving in
              Higher Order Logics
                (TPHOLs 2008)

      http://www.ece.concordia.ca/TPHOLs2008
           tphols08 <at> ece.concordia.ca

    August 18-21, 2008, Montreal, Quebec, Canada

The 2008 International Conference on Theorem Proving in Higher Order
Logics will be the 21st in a series that dates back to 1988. The
conference will be held in Montreal, Quebec, Canada, on 18-21 August 2008.

REGISTRATION

Registration is now open.  Please visit the TPHOLs 2008 web site,
http://www.ece.concordia.ca/TPHOLs2008/, to register.

INVITED SPEAKERS

Mike Gordon, University of Cambridge, UK.

  Twenty Years of Theorem Proving for HOLs

Steve Miller, Advanced Technology Center, Rockwell Collins, USA

   Will This Be Formal?
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gerwin Klein | 26 Aug 2008 07:05
Picon
Favicon

2nd CFP: JAR Special Issue on OS Verification

The deadline is drawing closer!

                             2nd Call for Papers

                Special Issue On Operating Systems Verification

                        Journal of Automated Reasoning

Industrial-strength software analysis and verification has advanced in recent
years through the introduction of model checking, automated and interactive
theorem proving, static analysis techniques, as well as correctness by
design. However, many techniques are working under restrictive assumptions
which are invalidated by complex (embedded) system software such as operating
system kernels, low-level device drivers or microcontroller code.

This special issue will be devoted to the formal verification of operating
systems and similar low-level systems code. The emphasis is on techniques and
methods that provide real solutions to real software problems. A real
solution is one that is applicable to the problem in industry and not one
that only applies to an abstract, academic toy version of it. Submissions are
encouraged, but not limited to, the following topics and their application to
operating systems or low-level systems code:

     * model checking
     * automated and interactive theorem proving
     * embedded systems development
     * programming languages
     * verifying compilers
     * software certification
(Continue reading)

Permalink | Reply | 0 comments |

Gmane