search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

[Cyclic Notation] Autoprover generates error #134

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Try to auto-prove the remaining sequent in: https://click-and-collect.linear-logic.org/?s=o&n=o%2C%21o+-o+o&cut_mode=1&p=%2FTd6WFoAAAD%2FEtlBA8CnAqYRIQEMAAAAKzhd3uAIpQEfXQA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJRzl9eyXig67oHQyYTslSub4UdC6wcpw%2BxPIisUM%2FDU96uPUsSW4WGq29bgUwwGLR5eRh%2BVD8DkMojLvBUaM6QT1Jmah2RSdgTk5pB3DOxBPjy61PwJv0%2B0wyl6st1gMFVaf5x1C68jfjbWYAU6LVh3%2B72VO%2B%2BtzfSFTdIU8Lfc1nEWMHVfY54NcHF4DYHJ1f5yvYr11eOTgX8WyhpAcsAiRcdpd7UglVs219ixrPS%2BdaqydukK6SE74HsHd0K4%2B9nIqhM9j9u7kM1H3FPesPrHWbWFO7QdjzPxwM3mKIj0NnAAQJQLeMc7ZhqbAwmWvgQwKWfue9iEMB%2BORTpGvAAAAAG3AqYRAADuK77LqAAK%2FAIAAAAAAFla

etiennecallies commented 3 years ago

I'm on it, there is a Stack_overflow error. I think it comes from usages of List.concat (List.map )(not tail-recursive) instead of List.concat_map (tail-recursive). I need to upgrade to Ocaml 4.10 or higher.