brando90

Simplified version of Dually Ground BackTranslation for AutoFormalization:

def train_to_af_for_maf(mdl : causal_lm,
                        formal_data_set, # e.g., ITP lib like mathlib
                        informal_data_set,  # e.g., time-tested maths textbook e.g., Rudin, CLRS.
                        ):
    for (nl, fl*) in formal_data_set; for (nl*, fl) in informal_data_set;
        # -- Learn to Formalize: nl_i->fl* from fl* -> [nl_i]_i -> fl*
        [nl_i]_i := mdl("informalize " + fl*, sampling=top_p, num_out=k)  # noise is good for robustness!

brando90

-- https://leanprover-community.github.io/lean-web-editor/#code=--%20Skipping%20importing%20default%20nat%20libraries%0A--%20import%20data.nat.basic%20--%20imports%20standard%20nats%20in%20lean%0A%0A----%201.%20Defining%20unary%20natural%20numbers%20%28could%20have%20defined%20it%20as%20my_nat%29%0Ainductive%20u_nat%20%3A%20Type%0A%7C%20zero%20%3A%20u_nat%20--%20%230%0A%7C%20succ%20%3A%20u_nat%20%E2%86%92%20u_nat%20--%20%231%0A--%20Open%20the%20namespace%20to%20use%20%60zero%60%20and%20%60succ%60%20without%20prefix.%20So%20you%20don't%20have%20to%20do%20unary_nat.zero%20or%20unary_nat.succ%0Aopen%20u_nat%0A%0A----%202.%20let's%20construct%20some%20natural%20numbers!%0A%23eval%20zero%0A--%20%23reduce%20zero%0A%23eval%20succ%20zero%0A--%20%23reduce%20succ%20zero%0A%23eval%20succ%28succ%20zero%29%0A--%20%23reduce%20succ%28succ%20zero%29%0A%0A------%203.%20Let's%20define%20addition%20recursively%20%28on%20the%20right%29%0Adef%20add%20%3A%20u_nat%20%E2%86%92%20u_nat%20%E2%86%92%20u_nat%20%0A--%20def%20add%20%28n%2

brando90

kinit brando9@CS.STANFORD.EDU

ssh brando9@login.sherlock.stanford.edu
ssh brando9@skampere1.stanford.edu


CS 197
/afs/ir/class/cs197

https://docs.google.com/document/d/1A3StDOlJCRBD4CSd44FSj_JxqnWhW7hbEjXqkJKFuvk/edit 

brando90

"""
Decision, chunk data up to having 4096 tokens which is approximately 3072 words which is approximately 16,896 chars. Then llama2's training/tokenizer can truncate to a max length i.e. 4096 if it's too long. 
(To avoid losing some context at the boundaries, we will include 50 chars from the end of previous sequence.)
https://chat.openai.com/c/d64d19cf-1261-44c9-bfa0-3472d327138e

refs:
- https://chat.openai.com/share/cec64728-9c40-4ce5-acb1-042019c1eb61
- https://claude.ai/chat/634c2a5f-675a-400b-9256-79e69cc02c6d
- https://huggingface.co/mafmaticians
"""

brando90

#!/usr/bin/env bash

# -- apt isn't recommended, always see official install isntructions
#RUN apt-get install -y --no-install-recommends rbenv
#RUN apt-get install -y --no-install-recommends ruby-build
#RUN apt-get install -y --no-install-recommends ruby-full
#RUN rbenv install 3.1.2
#RUN rbenv global 3.1.2

# -- apt isn't recommended, always see official install isntructions

brando90

context: https://stackoverflow.com/questions/74695464/why-cant-i-install-ruby-3-1-2-in-linux?noredirect=1#comment131843536_74695464

```
$ ruby-build --definitions
1.8.5-p52
1.8.5-p113
1.8.5-p114
1.8.5-p115
1.8.5-p231
1.8.6

brando90

```
conda install -c conda-forge opam 

...

This path already exists in the target prefix, and it won't be removed
by an uninstall action in this transaction. The path is one that conda
doesn't recognize. It may have been created by another package manager.

brando90

"""
Use this one to make sure the "end" is shown properly 100% etc
"""

import time
import progressbar

widgets = [
    progressbar.Percentage(),
    progressbar.Bar(),

brando90

(* -*- mode: ocaml; -*- *)

module type FUNCTOR = sig
  type 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}

type var = string

brando90

import subprocess

def talk_to_python_interactively():
    fw = open("tmpout", "wb")
    fr = open("tmpout", "r")
    p = subprocess.Popen(['python'],stdin=subprocess.PIPE,stdout=fw,stderr=fw,)
    out = frw.readline()
    print(out)
    print(len(out))
    print(type(out))