JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

Tutorial for "Console Application" Turning Up Error #343

Open brandon-sisler opened 3 months ago

brandon-sisler commented 3 months ago

Hey all, I am totally new to this and came to the issues page as a last resort when I couldn't get anything to work. I'm trying to install and use Arend using the method outlined in "Console Application" at " https://arend-lang.github.io/documentation/getting-started.html ". Let me walk you through what works.

  1. Downloading the jar file is fine.
  2. Running the test "java -jar Arend.jar" works fine and produces the expected result.
  3. Creating the directories and files goes on without a hitch, although that's all me really, so I don't think Arend could be to blame for issues there.
  4. Once I run the command " java -jar $arend $myProject " I have the return error "Error: -jar requires jar file specification."

So my question is, am I supposed to be putting in these $ signs, or am I supposed to somehow actually specify the path to the Arend.jar file and the arend.yaml file. If so, how do I do this (context: I know no java). Thanks!

ice1000 commented 3 months ago

am I supposed to somehow actually specify the path to the Arend.jar file and the arend.yaml file

Yes

sxhya commented 3 months ago

I would recommend you to try using Arend via plugin which is part of IntellijIDEA (it is available for Community Edition as well). If you would like to build Arend from sources I would recomment to download JetBrains/Arend GitHub repository and then make everything using ./gradlew jarDep command.