[MetaPRL Users] Re: help on metaprl editor screen (was Re:
Undefined_recursive_module during omake-boot
Yegor Bryukhov
ybryukhov at gmail.com
Fri Jun 6 10:28:00 PDT 2008
Hi Larry,
concerning #use "x.ml", I'm not sure that mp allows you to open source
files on the fly, but the rest of the editor tutorial should be
applicable, the browser interface just links certain commands to the
menu.
Note that "Creating new objects" section of the editor help page is
not the standard way to create objects, usually you create an .ml file
where all your objects are defined, register it in MetaPRL build
system and recompile MetaPRL.
You can also do "mp -cli" for old command line interface (but #use
does not work there either, at least for me)
On Fri, Jun 6, 2008 at 11:53 AM, Aleksey Nogin <nogin at metaprl.org> wrote:
> 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
>>
>
> _______________________________________________
> MetaPRL-Users mailing list
> MetaPRL-Users at metaprl.org
> https://lists.metaprl.org/mailman/listinfo/metaprl-users
>
--
Best regards,
Yegor
__________________________________________________________
Yegor Bryukhov,
Research Associate
Center for Algorithms and Interactive Scientific Software
City College of New York
More information about the MetaPRL-Users
mailing list