how do we copy files between repositories without losing the history?

how_to_copy_between_repos.md

Scenario

• We want to move all files under library/hott in leanprover/library repo to src/library/hott in leanprover/lean repo.
• We want to preserve the commit history of leanprover/library during the migration.

Solution

I assume that leanprover/lean repo is already cloned at ~/work/lean.

1. Add leanprover/libraries repo as a remote.

   cd ~/work/lean
   git remote add libs [email protected]:leanprover/libraries
   git fetch libs
   

2. Create a local branch libs based on libs/master.

   git co -b libs libs/master
   

3. Extract files under library/hott and move them to src/library/hott.

First, please save the following script as extract_and_move.

```bash

#!/usr/bin/env bash

extract_and_move: Extract files from and move them under

if [ ! $# -eq 2 ] then echo "./extract_and_move " exit 1 fi SRC=$1 DEST=$2 DEST_FIRST=${DEST%%/*}

Extract $SRC, put them at the project root

git filter-branch -f --prune-empty --subdirectory-filter $SRC -- HEAD

Move them under $DEST

git filter-branch -f --prune-empty --tree-filter "mkdir -p $DEST; find . -mindepth 1 -maxdepth 1 | grep -v ${DEST_FIRST} | grep -v '^./.git' | xargs -I {} mv {} ./$DEST" HEAD ```

and use:

    extract_and_move library/hott src/library/hott

4. Switch back to master branch

   git co master
   

5. Take commits in libs branch on top of master by rebase.

   git rebase --onto libs master master