Otter is an Automated Deduction System, From the Website: Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP. 3.2 is the latest version. Unfortunately the Licence doesn't seem to be in the Licences directory. (It's a U.S. Government one) I've hopefully attached it to this bug as 'Legal'. I would suggest app-sci/otter. This ebuild doens't depend on anything, as I can tell. Just being able to compile c programs, no particular version of glibc or anything is required. Reproducible: Always Steps to Reproduce: 1. 2. 3.
Created attachment 10434 [details] otter-3.2.ebuild ebuild file
Created attachment 10435 [details] Licence terms for otter
Created attachment 10436 [details] otter ebuild file - better version sorry about the first one. V-naughty of me.
Hi Meghan. Thanks for your submission! I have processed and committed the build. Please test. Few small notes: 1. it is best to use constructs like ${PN} ${P} where possible 2. it is better to use ${var} form instead of $var 3. You could have groupped mutiple dobin and dodoc's like this is now done in ebuild George
reclosing the bug
Bumped to 3.3, needed to do some adjustments, as build procedure slightly changed. Reclosing the bug. George
