Merge pull request #12 from trishullab/usr/amit9oct/license-changes

Created pip instructions.

Author: amit9oct

README.md

@@ -1,7 +1,27 @@
 # itp-interface
 Generic interface for hooking up to any Interactive Theorem Prover (ITP) and collecting data for training ML models for AI in formal theorem proving. 
 
-## Setup Steps:
+## Quick Setup for Lean 4:
+1. Install itp-interface using the following command:
+```bash
+pip install itp-interface
+```
+
+2. Run the following command to prepare the REPL for Lean 4. (The default version is 4.7.0-rc2. You can change the version by setting the `LEAN_VERSION` environment variable. If no version is set, then 4.7.0-rc2 is used.)
+>NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with.
+```bash
+export LEAN_VERSION="4.15.0"
+install-lean-repl
+```
+
+3. Run the following command to build the REPL for Lean 4. Make sure that `lean --version` returns the correct version before running the command below. If not then check if `$HOME/.elan/bin` is in your path. Recommended to run `source $HOME/.elan/env` before running the command below.
+```bash
+install-itp-interface
+```
+
+>NOTE: These steps are only tested on Linux. For Windows, you can use WSL. These steps will not setup the Coq interface.
+
+# Full Setup for Coq and Lean:
 1. Install OCaml first. Use the instructions here: https://opam.ocaml.org/doc/Install.html . The opam version used in this project is 2.1.3 (OCaml 4.14.0). Note that OCaml officially only supports Linux installations. One can use WSL on Windows machines.
 
 2. Run the following to install Coq on Linux. The Coq version used in this project is <= 8.15. 
@@ -17,25 +37,28 @@ export PATH="/home/$USER/.opam/default/bin:$PATH"
 
 4. Create a `Miniconda` environment and activate it.
 
+5. Run the commands for installing the Lean 4 interface as mentioned in [Quick Setup for Lean 4](#quick-setup-for-lean-4).
 
-5. Change to the project root directory, and run the setup script i.e. `./src/scripts/setup.sh` from the root directory.
+6. Change to the project root directory, and run the setup script i.e. `./src/scripts/setup.sh` from the root directory.
 
-6. Add the following to your `.bashrc` file for Lean:
+7. Add the following to your `.bashrc` file for Lean:
 ```
 export PATH="/home/$USER/.elan/bin:$PATH"
 ```
 
-7. You need to run the following command to generate sample proof step data for Lean 4:
+## Generating Proof Step Data:
+
+1.a. You need to run the following command to generate sample proof step data for Lean 4:
 ```
 python src/itp_interface/main/run_tool.py --config-name simple_lean_data_gen
 ```
 Check the `simple_lean_data_gen.yaml` configuration in the `src/itp_interface/configs` directory for more details. These config files are based on the `hydra` library (see [here](https://hydra.cc/docs/intro/)).
 
-8. You need to run the following command to generate sample proof step data for Coq:
+1.b. You need to run the following command to generate sample proof step data for Coq:
 ```
 python src/itp_interface/main/run_tool.py --config-name simple_coq_data_gen
 ```
-Check the `simple_coq_data_gen.yaml` configuration in the `src/itp_interface/configs` directory for more details.
+Check the `simple_coq_data_gen.yaml` configuration in the `src/itp_interface/configs` directory for more details about where the generated data is stored and where the different ITP (Coq and Lean) projects are located in the file system.
 
-## Important Notes:
+## Important Note:
 The ITP projects must be built before running proof step data generation. Make sure that the switch is set correctly while generating data for Coq projects because the Coq projects can be using different versions of Coq. Instructions for Coq project setup are listed in `src/itp_interface/main/config/repo/coq_repos.yaml` file.

pyproject.toml

@@ -45,4 +45,5 @@ Homepage = "https://github.com/trishullab/itp-interface"
 Issues = "https://github.com/trishullab/itp-interface/issues"
 
 [project.scripts]
-install-itp-interface = "itp_interface.main.install:install_itp_interface"
+install-itp-interface = "itp_interface.main.install:install_itp_interface"
+install-lean-repl = "itp_interface.main.install:install_lean_repl"

src/itp_interface/main/install.py

@@ -10,4 +10,83 @@ def install_itp_interface():
     assert os.path.exists(os.path.join(repl_dir, "lean-toolchain")), f"lean-toolchain does not exist in {repl_dir}, build has failed"
     print("repl_dir: ", repl_dir)
     print("Building itp_interface")
-    os.system(f"cd {repl_dir} && lake build repl")
+    os.system(f"cd {repl_dir} && lake build repl")
+
+def install_lean_repl():
+    print("Updating Lean")
+    itp_dir = os.path.dirname(os.path.dirname(file_path))
+    tools_dir = os.path.join(itp_dir, "tools")
+    repl_dir = os.path.join(tools_dir, "repl")
+    assert os.path.exists(repl_dir), f"repl_dir: {repl_dir} does not exist"
+    assert os.path.exists(os.path.join(repl_dir, "lean-toolchain")), f"lean-toolchain does not exist in {repl_dir}, build has failed"
+    print("repl_dir: ", repl_dir)
+    assert os.system("git --version") == 0, "git is not installed"
+    print("[OK] git is installed")
+    print("Checking if Lean version is set in environment variables as LEAN_VERSION")
+    print("If not, defaulting to 4.7.0-rc2")
+    lean_version = os.environ.get("LEAN_VERSION", "4.7.0-rc2")
+    github_repo = "https://github.com/amit9oct/repl.git"
+    if lean_version.strip() == "4.7.0-rc2":
+        print("Lean version is set to 4.7.0-rc2, not cloning the REPL")
+    else:
+        # Clone the repl fresh
+        print("Cloning the REPL fresh")
+        os.system(f"rm -rf {repl_dir}")
+        os.system(f"git clone {github_repo} {repl_dir}")
+        # escape the version number
+        lean_version_esc = lean_version.replace(".", "\.")
+        print("Switching to the right REPL version", lean_version_esc)
+        cmd_to_run = f"cd {repl_dir} && git log --grep \"v{lean_version_esc}\" --pretty=\"%h %s\""
+        print("Running: ", cmd_to_run)
+        output = os.popen(cmd_to_run).read()
+        print("Output: ", output)
+        if output == "":
+            print(f"Could not find a commit with message containing {lean_version}")
+            print("Probably this version does not exist in the git history of the REPL")
+            lean_version = "4.7.0-rc2"
+            print("Switching to v4.7.0-rc2 on commit 97182f0")
+            os.system(f"cd {repl_dir} && git checkout 97182f0")
+        else:
+            # Split on first space
+            for line in output.split("\n"):
+                if line:
+                    commit, message = line.split(" ", 1)
+                    if lean_version in message:
+                        print(f"Switching to commit {commit}")
+                        os.system(f"cd {repl_dir} && git checkout {commit}")
+                        break
+    # Make sure that .elan is installed
+    print("Checking if .elan is installed")
+    if os.path.exists(os.path.expanduser("~/.elan")):
+        print("[OK] .elan is installed")
+    else:
+        print("Installing .elan")
+        elan_url = "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh"
+        os.system(f"curl -sSL {elan_url} | sh")
+        print("[OK] .elan installed")
+        lean_repo = "leanprover-community/lean"
+        # Create a temporary script to run
+        shell_code = f"""
+source $HOME/.elan/env
+echo "Installing Lean 4 ({lean_repo}:{lean_version})..."
+elan toolchain install {lean_repo}:{lean_version}
+elan override set {lean_repo}:{lean_version}
+echo "Installed Lean 4 ({lean_repo}:{lean_version}) successfully!"
+export PATH=$PATH:$HOME/.elan/bin
+"""
+        random_string = os.urandom(8).hex()
+        with open(f"/tmp/{random_string}.sh", "w") as f:
+            f.write(shell_code)
+        os.system(f"chmod +x /tmp/{random_string}.sh")
+        print("Running the script")
+        os.system(f"bash /tmp/{random_string}.sh")
+        print("Removing the script")
+        os.system(f"rm /tmp/{random_string}.sh")
+        assert os.system("lean --version") == 0, "Lean 4 is not installed aborting"
+        print("[OK] Lean 4 installed successfully")
+    print("NOTE: Please run `install-itp-interface` to finish the installation")
+
+
+            
+    
+