Dear Adnan,
the expected way to use Multivariate/cauchy.ml is by loading the file
Multivariate/make_complex.ml which in turn loads all the dependencies in
the appropriate order (including cauchy.ml).
You also must be warned that loading complex analysis may take a while (say
30 minutes, but obviously it depends on your setting).
Hope it helps,
Marco
2015-02-13 9:32 GMT+01:00 Adnan Rashid <[email protected]>:
> Dear all,
>
> I am using Hol-light on Ubuntu 14.04. I am facing theory loading conflict.
> I am loading only two theories in alternative sequences but in both cases I
> am having problems. The theories are *Multivariate/cauchy.ml
> <http://cauchy.ml>* and *Library/poly.ml <http://poly.ml>*.
>
> In the first case, when I load cauchy theory first, it ends up with the
> following error:
>
>
> -------------------------------------------------------------------------------
>
> File "/home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml",
> line 12911, characters 35-58:
> Error: Unbound value REAL_LOG_CONVEX_ON_SING
> Error in included file
> /home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
> val it : unit = ()
>
>
> -------------------------------------------------------------------------------
>
> After this, I load the poly theory which also ends up with the following
> error:
>
>
> -------------------------------------------------------------------------------
>
> File "/home/user/hol-light-workbench/hol-light/Library/poly.ml", line
> 173, characters 51-61:
> Error: Unbound value DIFF_CONST
> Error in included file /home/user/hol-light-workbench/hol-light/Library/
> poly.ml
> val it : unit = ()
>
>
> -------------------------------------------------------------------------------
>
> In this sequence of loading theories, it does not recognize the theorems
> when entered in shell.
> e.g.
>
> *REAL_CONTINUOUS_ATREAL_WITHINREALError: Unbound value
> REAL_CONTINUOUS_ATREAL_WITHINREAL*
>
> Where as, in the second case, when I load poly theory first, it ends up
> fine. Next, when I load the cauchy theory, it ends up with the following
> error:
>
>
> ---------------------------------------------------------------------------------
>
> Error in included file
> /home/user/hol-light-workbench/hol-light/Multivariate/realanalysis.ml
> - : unit = ()
> File "/home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml",
> line 23, characters 45-64:
> Error: Unbound value OPEN_CONTAINS_CBALL
> Error in included file
> /home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml
> - : unit = ()
> - : unit = ()
> - : unit = ()
> Exception:
> Failure
> "typechecking error (initial type assignment): f cannot have type
> real->(_->bool)->bool and real->real simultaneously".
> Error in included file
> /home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
> val it : unit = ()
>
>
> ------------------------------------------------------------------------------
>
> In this case, when I write a goal involving exponential (exp) function, it
> gives error* Exception: Noparse* else it works fine.
>
> If I try only cauchy theory without loading poly theory, it results no
> error when using exp function, which, to me, shows that *Noparse* error
> is not due to brackets.
>
> Thanks in advance.
>
>
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming. The Go Parallel Website,
> sponsored by Intel and developed in partnership with Slashdot Media, is
> your
> hub for all things parallel software development, from weekly thought
> leadership blogs to news, videos, case studies, tutorials and more. Take a
> look and join the conversation now. http://goparallel.sourceforge.net/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
