search

meta-logic / sellf

SubExponential Linear Logic Framework for reasoning about sequent calculus systems
7 stars 2 forks source link

Quati: Download LaTeX button #7

Open leonardolima opened 7 years ago

leonardolima commented 7 years ago

The content downloaded doesn't refresh after the first time, i.e., if we select a pair of rules and after that we try another pair (we can keep going), the content to be downloaded is associated to the first pair and will not change. Obviously, this only happens on the tab 'permutations.'

leonardolima commented 7 years ago

fcbc5f6ca587e6cb52dab3a77d3012594e1f00ad was not enough to fix this. It should be a bug on the function permute_to_file in sellf.ml, but it might be a good idea to refactor all these print functions, there is no pattern and the entire file is a mess.

leonardolima commented 5 years ago

I'm pretty sure commit e12ccde846271360cee94f5fb8abd0c9f3598608 will fix this issue. However, it will take a while before changes go live because permutations don't seem to be working properly in the current version of SELLF. We should probably discuss this @gisellemnr :)

gisellemnr commented 5 years ago

What is the problem with permutations?

leonardolima commented 5 years ago 
[~/sellf/src]$ ./tests.permutations
------------------ Testing LL ------------------------

** tensor left permutes up: 
x----> tensor right? Expected No. Got N/A.
x----> tensor left? Expected Yes. Got N/A.
x----> lolli right? Expected Yes. Got N/A.
x----> lolli left? Expected No. Got N/A.
x----> plus right? Expected Yes. Got N/A.
[...]

Correct results: 9
Wrong results: 95

I'm not exactly sure, but in all cases Quati cannot build the derivations.

gisellemnr commented 5 years ago

That's odd... when I run the script here, I see:

Correct results: 76
Wrong results: 28

Do you have uncommitted changes?

leonardolima commented 5 years ago

I don't. I've tried to clone the rep again but the results were exactly the same.

I'm gonna try to execute it on the server.

gisellemnr commented 5 years ago

I also tried cloning the repo again, but I still have 76/28 right/wrong results. Maybe it is a version issue?

In my machine, I have:

The OCaml toplevel, version 4.07.0

and

DLV [build BEN/Dec 17 2012   gcc 4.6.1]