[MetaPRL Users] Re: help on metaprl editor screen (was Re: Undefined_recursive_module during omake-boot

[Aleksey Nogin]

Larry,

I just got a second baby yesterday, so will be unavailable for a while. 
I am forwarding this to metaprl-users, I am sure somebody else will be 
able to help.

Aleksey

On 05.06.2008 10:57, Larry Evans wrote:

> On 05/20/08 13:38, Larry Evans wrote:
>> On 05/20/08 13:15, Aleksey Nogin wrote:
>>> On 20.05.2008 10:54, Larry Evans wrote:
>>>
>>>>> And are you using the latest SVN of MetaPRL, or some other version?
>>>>>
>>>> The metaprl was  downloaded from:
>>>>
>>>>    http://files.metaprl.org/MetaPRL-SVN-2007.05.06.tar.bz2
>>>>
>>> Oh, that might explain it - the tarballs collection was obviously 
>>> unmaitained for a while. I would recommend running "svn up" to get 
>>> the latest version - hopefully this would bring in whatever fixes 
>>> needed.
>>>
>>> Aleksey
>>>
>> Yes!  I've now got the
>>
>>
>>    Welcome To MetaPRL
>>
>>
>> screen.  Thanks very much!
>>
> Dear Sir:
> 
> Thanks for helping me get the mp editor working; however, I'm not
> trying to use the editor.  I'm using the browser interface and the
> location bar on the browser has:
> 
> https://evansl-desktop:60000/session/1/frameset
> 
> The editor screen has something like the
> following:
> <--- cut here ---
> 
> |>file  |>Edit  |>View  |>Directory  |>Proof  |>Refine  |>Help
> 
> Location: /
> Root Theories Listing:
> RootTheory "base": Basic Meta-Theory
> RootTheory "itt_core": Computational Type Theory (Core Logic)
> RootTheory "support": MetaPRL Internal "Helper" Modules
> RootTheory "fs": Browse MetaPRL Source Code
> end
> 
> 
> 
> 
> 
> 
> 
> |Submit  |Clear  |Long  |>History
> 
> 
> #_______________________________________...
> 
>  >--- cut here ---
> 
> If I enter a simple expression, 1+2, after the # and press the |Submit
> button, the result is:
> 
> <--- cut here ---
> 
> |>file  |>Edit  |>View  |>Directory  |>Proof  |>Refine  |>Help
> 
> Location: /
> Root Theories Listing:
> RootTheory "base": Basic Meta-Theory
> RootTheory "itt_core": Computational Type Theory (Core Logic)
> RootTheory "support": MetaPRL Internal "Helper" Modules
> RootTheory "fs": Browse MetaPRL Source Code
> end
> 
> 
> 
> 
> 
> 
> 
> 
> # 1+2
> 3 : int
> |Submit  |Clear  |Long  |>History
> 
> #_______________________________________...
> 
>  >--- cut here ---
> The file:
> 
>  http://metaprl.org/user-guide/default.html
> 
> does not show these screens.  It seems to be describing
> a commandline interface instead of a browser interface.
> 
> The */user-guide/default.html contains:
> 
>  For the OCaml toploop, you will need to open several modules before
>  you can get started. The common modules are defined in the file
>  x.ml, your first action would be to evaluate this file:
> 
> 
>    % editor/ml/mp
>    MetaPRL version 0.1
>    # #use "x.ml"
> 
> However, when I entered:
> 
>    #use "x.ml"
>   into the line starting with # at the bottom of the browser screen, I
> got:
> 
>     # use "x.ml"
>    Line 1, characters 1-3:
>    LinRefine error:
>    LinRefiMptop.mk_var_expr: undefined variable use
>   Could you let me know what I should do or what other documentation is
> available to guide me through the browser interface.  I did try to
> use other commands (besides mptop) in the lib directory:
> 
>   /home/evansl/download/metaprl/svn/metaprl/lib:
>  wildcard mp*
>  lrwxrwxrwx 1 evansl evansl 29 May 20 13:33 mpdebug-top -> 
> ../support/editor/mpdebug-top
>  lrwxrwxrwx 1 evansl evansl 27 May 20 13:34 mpkonsole -> 
> ../support/editor/mpkonsole
>  lrwxrwxrwx 1 evansl evansl 33 May 20 13:34 mpkonsole-large -> 
> ../support/editor/mpkonsole-large
>  lrwxrwxrwx 1 evansl evansl 25 May 20 13:33 mpshell -> 
> ../support/editor/mpshell
>  lrwxrwxrwx 1 evansl evansl 23 May 20 13:34 mptop -> 
> ../support/editor/mptop
>  lrwxrwxrwx 1 evansl evansl 25 May 20 13:34 mpxterm -> 
> ../support/editor/mpxterm
>  lrwxrwxrwx 1 evansl evansl 31 May 20 13:33 mpxterm-large -> 
> ../support/editor/mpxterm-large
> 
> however all of them gave some sort of error message.  The file used
> to start the browser interface was the mp file found here:
> 
>   /home/evansl/download/metaprl/svn/metaprl/editor/ml:
>  wildcard mp*
>  lrwxrwxrwx 1 evansl evansl       15 May 20 13:34 mp -> ../../lib/mptop
>  -rwxr-xr-x 1 evansl evansl 21012081 May 20 13:34 mp.top
>  -rw-r--r-- 1 evansl evansl      759 May 20 13:34 mpconfig
>  lrwxrwxrwx 1 evansl evansl       21 May 20 13:33 mpdebug-top -> 
> ../../lib/mpdebug-top
>  lrwxrwxrwx 1 evansl evansl       19 May 20 13:34 mpkonsole -> 
> ../../lib/mpkonsole
>  lrwxrwxrwx 1 evansl evansl       25 May 20 13:34 mpkonsole-large -> 
> ../../lib/mpkonsole-large
>  lrwxrwxrwx 1 evansl evansl       17 May 20 13:33 mpshell -> 
> ../../lib/mpshell
>  lrwxrwxrwx 1 evansl evansl       15 May 20 13:34 mptop -> ../../lib/mptop
>  lrwxrwxrwx 1 evansl evansl       17 May 20 13:34 mpxterm -> 
> ../../lib/mpxterm
>  lrwxrwxrwx 1 evansl evansl       23 May 20 13:33 mpxterm-large -> 
> ../../lib/mpxterm-large
> 
> which, of course, is symlinked to the mptop command.
> 
> I realize this is a lot of trouble for a non-student and I appreciate
> any time you could spare to help me or suggest other resources to help
> me.
> 
> -regards,
> Larry
>