On MacOSX, follow these steps: http://www.reed.edu/data-at-reed/software/R/r_studio.html
- Install R
- Install RStudio
- Download the
startup_packages.Rscript from that page:
| /* | |
| * Copyright 2016 California Institute of Technology ("Caltech"). | |
| * U.S. Government sponsorship acknowledged. | |
| * | |
| * Licensed under the Apache License, Version 2.0 (the "License"); | |
| * you may not use this file except in compliance with the License. | |
| * You may obtain a copy of the License at | |
| * | |
| * http://www.apache.org/licenses/LICENSE-2.0 | |
| * |
| package cafe | |
| import java.lang.{Integer,System} | |
| import fs2._ | |
| import scala.{App,Long,StringContext} | |
| object Main1 extends App { |
| package tags | |
| import frameless.{TypedColumn, TypedDataset} | |
| import frameless.ops.SmartProject | |
| import frameless.{CatalystCast, Injection} | |
| import org.apache.spark.SparkConf | |
| import org.apache.spark.sql.SparkSession | |
| import scala.{App,Int} | |
| import scala.Predef.{require,String} |
On MacOSX, follow these steps: http://www.reed.edu/data-at-reed/software/R/r_studio.html
startup_packages.R script from that page:| -----BEGIN PGP PUBLIC KEY BLOCK----- | |
| mQINBFz4QfkBEADka2rH/kSD1vvNvVT9E04N14pRi4s9qg7lu2i4vsXLOKOO49nR | |
| YHCN3DVM1FnPNdkb3kHThvPZh+afTsAzJDa2GG51A+Kfr3+vrZTEBvuCuFFHP8Dd | |
| zUw38csHjWBMex4RQ7Hil6tnuJ3BHKwhC2rmRDjnyv5hYaDhclW1rC8k1yheX4Z7 | |
| 27jYe0H2M4Gb4BebdtzFZzOI7Iz+1GBCqyZPc/QC8eoVrgzrZ6YkrmmxrqREYQLf | |
| qbze3KGhju+nC/AymrThykvQ54l/myCBcU4BVqJWl0uUsvm5xnQgEUqlnxebI2iC | |
| 7lq3KiKhflTqHYhTgcln2y04TDQNJ+/jxOSbM5TKCbMb+WPPSBHNH3XbmsjvmUDs | |
| +yqcWXcodAfhAes9RckTT5EkjAMdfMEbWxLS+6JV3cHetZGlhsRLSVZgqeyCQ1H6 | |
| BUrQ8Gbp66+fz45cYlZDnYT/8AZGIx+CjOeTe8IhjNTwhwdYheeMBEvDioFtbtww |
| -- A basic framework for graph theory on multidigraphs in Lean | |
| -- and a proof that no_watershed_condition is sufficient to | |
| -- establish that a graph has a unique sink for each vertex | |
| -- | |
| -- I hope to give some introduction to the syntax of how Lean works here, | |
| -- but I assume some familiarity with functions, pattern matching, | |
| -- type theory, and proofs. | |
| -- | |
| -- The most important thing to note is that `begin` and `end` delineate | |
| -- sections of code in "tactic/interactive proof mode" (as opposed to |