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.R
script 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 |