Execution of rumm

[agra-jorge]

Hi, just forked this repo and am trying to run some example. New to rust, can you pls point me to the right direction?

Best regards JA

[tirix]

Hi Jorge!

Ok, so a warning beforehand: this is pretty experimental, and not much made for ease of use.

As it is now, (see first line in example.mm) you need the following directory hierarchy:

|- set.mm (git clone)
|    - set.mm (the database file itself)
|- rumm (git clone)
     - rumm (rum directory within the clone)

That it, you need to clone set.mm and rumm at the same directory level.

At its core rumm works with Grammar parsing of set.mm, and it turns out that there must have been changes recently which broke that functionality. I picked one commit which still works. You can check it out using this command in your set.mm repository:

git checkout 57058dd0cdb1a09ca93fe39d71be95c4827c0689

And then you need to change directly to rumm/rumm and "simply" run cargo run. If everything goes well, you should see this:

Loading "examples/examples.mm" ... ok
Building "examples/examples.mm" grammar... ok
Parsing "examples/examples.mm"... ok
====================================================

Proof for "rummex1":
Proving |- ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( -u A x. ( ( B - C ) / D ) ) e. RR )
>> Use reals_closure
 Proving |- ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( -u A x. ( ( B - C ) / D ) ) e. RR )
 >> Try
 Proving |- ( ( ( A e. RR /\ B e. RR ) /\ C e. RR ) -> ( -u A x. ( ( B - C ) / D ) ) e. RR )

A lot of prints, and finally

45:36,42,8,9,44:ovmpt2d     |- ( ph -> ( A ( midG ` G ) B ) = ( iota_ m e. P B = ( ( S ` m ) ` A ) ) )
46:45:eqeq1d               |- ( ph -> ( ( A ( midG ` G ) B ) = M <-> ( iota_ m e. P B = ( ( S ` m ) ` A ) ) = M ) )
qed:17,46:bitr4d          |- ( ph -> ( B = ( ( S ` M ) ` A ) <-> ( A ( midG ` G ) B ) = M ) )

$=    ( vm va vb vg cfv wceq cv wcel fveq2d cvv cbs crio cmid co wreu clng eqid
      wb mideu id fveq1d eqeq2d riota2 syl2anc cmir cmpt2 cmpt df-mid a1i simpr
      syl6eqr riotaeqbidv mpt2eq123dv cstrkg elexd fvex eqeltri mpt2exga fvmptd
      wa simplr eqeq12d riotabidv anasss riotaex ovmpt2d eqeq1d bitr4d ) ACBHEU
      CZUCZUDZCBSUEZEUCZUCZUDZSDUJZHUDZBCFUKUCZULZHUDAHDUFWMSDUMWIWOUPRASBCDEFG
      FUNUCZIJKLWRUOMQOPNUQWMWISDHWJHUDZWLWHCWSBWKWGWSWJHEWSURUGUSUTVAVBAWQWNHA
      TUABCDDUAUEZTUEZWKUCZUDZSDUJZWNWPUHAUBFTUAUBUEZUIUCZXFWTXAWJXEVCUCZUCZUCZ
      UDZSXFUJZVDZTUADDXDVDZUHUKUHUKUBUHXLVEUDAUBSTUAVFVGAXEFUDZVRZTUAXFXFXKDDX
      DXOXFFUIUCZDXOXEFUIAXNVHZUGJVIZXRXOXJXCSXFDXRXOXIXBWTXOXAXHWKXOWJXGEXOXGF
      VCUCEXOXEFVCXQUGQVIUSUSUTVJVKAFVLMVMADUHUFZXSXMUHUFXSADXPUHJFUIVNVOVGZXTT
      UADDXDUHUHVPVBVQAXABUDZWTCUDZXDWNUDAYAVRZYBVRZXCWMSDYDWTCXBWLYCYBVHYDXABW
      KAYAYBVSUGVTWAWBOPWNUHUFAWMSDWCVGWDWEWF $.

$)

If you see that, you've successfully run rumm, which has successfully built proofs for a 5 example theorems, using it tactics-based system, following instructions in set.rmm.

Once you're there, you can play more, for example edit set.rmm to prove more theorems.

[tirix]

Note: This repository is an experiment I wrote to find out whether one could write a tactics-based proof assistant for Metamath. The answer is yes, but much more work needs to flow into it until it is usable.

If you've reached the limits of metamath-lamp and you'd like to use more established tools than rumm to write metamath proofs, I'd rather recommend Glauco's Yamma, or MMJ2.

[agra-jorge]

Worked, thanks.

Understand its experimental, no problem, on the contrary.

Best regards.

[tirix]

Nice!

If you'd like to check out the latest changes, they are in the trace-view branch. In that branch, the traces are dumped into an HTML file instead of the standard output, so you'll have a clean output, but all the details about the proof process in the HTML tree view.

Ideally, we'd have an assistant showing the current subgoal at each level, and highlighting where the proof currently fails.

Anyway I'll close this issue for now, if you have any further question don't hesitate to reach out.